src/ZF/Constructible/Relative.thy
changeset 13316 d16629fd0f95
parent 13306 6eebcddee32b
child 13319 23de7b3af453
     1.1 --- a/src/ZF/Constructible/Relative.thy	Mon Jul 08 17:24:07 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Mon Jul 08 17:51:56 2002 +0200
     1.3 @@ -753,11 +753,10 @@
     1.4  	     order_isomorphism(M,par,r,x,mx,g))"
     1.5    and obase_equals_separation:
     1.6       "[| M(A); M(r) |] 
     1.7 -      ==> separation
     1.8 -      (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
     1.9 -	      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
    1.10 -	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
    1.11 -	      order_isomorphism(M,pxr,r,y,my,g))))"
    1.12 +      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
    1.13 +			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
    1.14 +			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
    1.15 +			      order_isomorphism(M,pxr,r,y,my,g))))"
    1.16    and omap_replacement:
    1.17       "[| M(A); M(r) |] 
    1.18        ==> strong_replacement(M,