mmtheorems28 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 2701-2800 - Page 28 of 123

Type	Label	Description
Statement
Theorem	breq12i 2701	Equality inference for a binary relation. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &   |- C = D   =>   |- (ARC <-> BRD)
Theorem	breq1d 2702	Equality deduction for a binary relation.
|- (ph -> A = B)   =>   |- (ph -> (ARC <-> BRC))
Theorem	breq2d 2703	Equality deduction for a binary relation.
|- (ph -> A = B)   =>   |- (ph -> (CRA <-> CRB))
Theorem	breq12d 2704	Equality deduction for a binary relation.
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (ARC <-> BRD))
Theorem	breqan12d 2705	Equality deduction for a binary relation.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ph /\ ps) -> (ARC <-> BRD))
Theorem	breqan12rd 2706	Equality deduction for a binary relation.
|- (ph -> A = B)   &   |- (ps -> C = D)   =>   |- ((ps /\ ph) -> (ARC <-> BRD))
Theorem	eqbrtri 2707	Substitution of equal classes into a binary relation.
|- A = B   &   |- BRC   =>   |- ARC
Theorem	eqbrtrd 2708	Substitution of equal classes into a binary relation.
|- (ph -> A = B)   &   |- (ph -> BRC)   =>   |- (ph -> ARC)
Theorem	eqbrtrri 2709	Substitution of equal classes into a binary relation.
|- A = B   &   |- ARC   =>   |- BRC
Theorem	eqbrtrrd 2710	Substitution of equal classes into a binary relation.
|- (ph -> A = B)   &   |- (ph -> ARC)   =>   |- (ph -> BRC)
Theorem	breqtri 2711	Substitution of equal classes into a binary relation.
|- ARB   &   |- B = C   =>   |- ARC
Theorem	breqtrd 2712	Substitution of equal classes into a binary relation.
|- (ph -> ARB)   &   |- (ph -> B = C)   =>   |- (ph -> ARC)
Theorem	breqtrri 2713	Substitution of equal classes into a binary relation.
|- ARB   &   |- C = B   =>   |- ARC
Theorem	breqtrrd 2714	Substitution of equal classes into a binary relation.
|- (ph -> ARB)   &   |- (ph -> C = B)   =>   |- (ph -> ARC)
Theorem	3brtr3i 2715	Substitution of equality into both sides of a binary relation.
|- ARB   &   |- A = C   &   |- B = D   =>   |- CRD
Theorem	3brtr4i 2716	Substitution of equality into both sides of a binary relation.
|- ARB   &   |- C = A   &   |- D = B   =>   |- CRD
Theorem	3brtr3d 2717	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> CRD)
Theorem	3brtr4d 2718	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> CRD)
Theorem	3brtr3g 2719	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- A = C   &   |- B = D   =>   |- (ph -> CRD)
Theorem	3brtr4g 2720	Substitution of equality into both sides of a binary relation.
|- (ph -> ARB)   &   |- C = A   &   |- D = B   =>   |- (ph -> CRD)
Theorem	syl5eqbr 2721	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- C = A   =>   |- (ph -> CRB)
Theorem	syl5eqbrr 2722	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- A = C   =>   |- (ph -> CRB)
Theorem	syl5breq 2723	A chained equality inference for a binary relation.
|- (ph -> A = B)   &   |- CRA   =>   |- (ph -> CRB)
Theorem	syl5breqr 2724	A chained equality inference for a binary relation.
|- (ph -> B = A)   &   |- CRA   =>   |- (ph -> CRB)
Theorem	syl6eqbr 2725	A chained equality inference for a binary relation.
|- (ph -> A = B)   &   |- BRC   =>   |- (ph -> ARC)
Theorem	syl6eqbrr 2726	A chained equality inference for a binary relation.
|- (ph -> B = A)   &   |- BRC   =>   |- (ph -> ARC)
Theorem	syl6breq 2727	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- B = C   =>   |- (ph -> ARC)
Theorem	syl6breqr 2728	A chained equality inference for a binary relation.
|- (ph -> ARB)   &   |- C = B   =>   |- (ph -> ARC)
Theorem	ssbrd 2729	Deduction from a subclass relationship of binary relations.
|- (ph -> A (_ B)   =>   |- (ph -> (CAD -> CBD))
Theorem	ssbri 2730	Inference from a subclass relationship of binary relations.
|- A (_ B   =>   |- (CAD -> CBD)
Theorem	hbbr 2731	Bound-variable hypothesis builder for binary relation.
|- (y e. A -> A.x y e. A)   &   |- (y e. R -> A.x y e. R)   &   |- (y e. B -> A.x y e. B)   =>   |- (ARB -> A.x ARB)
Theorem	hbbrd 2732	Deduction version of bound-variable hypothesis builder hbbr 2731.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   &   |- (ph -> (y e. R -> A.x y e. R))   &   |- (ph -> (y e. B -> A.x y e. B))   =>   |- (ph -> (ARB -> A.x ARB))
Theorem	brab1 2733	Relationship between a binary relation and a class abstraction.
|- (xRy <-> x e. {z | zRy})
Theorem	brprc 2734	A property of proper class as the second argument of a binary relation.
|- (-. B e. V -> (ARB <-> ARA))
Theorem	brun 2735	The union of two binary relations.
|- (A(R u. S)B <-> (ARB \/ ASB))
Theorem	sbcbrg 2736	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> [_A / x]_B[_A / x]_R[_A / x]_C))
Theorem	sbcbr12g 2737	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> [_A / x]_BR[_A / x]_C))
Theorem	sbcbr1g 2738	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> [_A / x]_BRC))
Theorem	sbcbr2g 2739	Move substitution in and out of a binary relation.
|- (A e. D -> ([A / x]BRC <-> BR[_A / x]_C))
Ordered-pair class abstractions (class builders)
Syntax	copab 2740	Extend class notation to include ordered-pair class abstraction (class builder).
class {<.x, y>. | ph}
Definition	df-opab 2741	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it (see dfid2 2915 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 4173.
|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
Theorem	opabss 2742	The collection of ordered pairs in a class is a subclass of it.
|- {<.x, y>. | xRy} (_ R
Theorem	opabbid 2743	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})
Theorem	opabbidv 2744	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})
Theorem	opabbii 2745	Equivalent wff's yield equal class abstractions.
|- (ph <-> ps)   =>   |- {<.x, y>. | ph} = {<.x, y>. | ps}
Theorem	cbvopab 2746	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution.
|- (ph -> A.zph)   &   |- (ph -> A.wph)   &   |- (ps -> A.xps)   &   |- (ps -> A.yps)   &   |- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, w>. | ps}
Theorem	cbvopabv 2747	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution.
|- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, w>. | ps}
Theorem	cbvopab1 2748	Change first bound variable in an ordered-pair class abstraction, using explicit substitution.
|- (ph -> A.zph)   &   |- (ps -> A.xps)   &   |- (x = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, y>. | ps}
Theorem	cbvopab1s 2749	Change first bound variable in an ordered-pair class abstraction, using explicit substitution.
|- {<.x, y>. | ph} = {<.z, y>. | [z / x]ph}
Theorem	cbvopab1v 2750	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)
|- (x = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, y>. | ps}
Theorem	cbvopab2v 2751	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution.
|- (y = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.x, z>. | ps}
Theorem	csbopabg 2752	Move substitution into a class abstraction.
|- (A e. B -> [_A / x]_{<.y, z>. | ph} = {<.y, z>. | [A / x]ph})
Theorem	unopab 2753	Union of two ordered pair class abstractions.
|- ({<.x, y>. | ph} u. {<.x, y>. | ps}) = {<.x, y>. | (ph \/ ps)}
Transitive classes
Syntax	wtr 2754	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr A
Definition	df-tr 2755	Define a transitive class. Not to be confused with a transitive relation (see cotr 3528). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 2756 (which is suggestive of the word "transitive"), dftr3 2758, dftr4 2759, dftr5 2757, and (when A is a set) unisuc 3049. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130.
|- (Tr A <-> U.A (_ A)
Theorem	dftr2 2756	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40.
|- (Tr A <-> A.xA.y((x e. y /\ y e. A) -> x e. A))
Theorem	dftr5 2757	An alternate way of defining a transitive class.
|- (Tr A <-> A.x e. A A.y e. x y e. A)
Theorem	dftr3 2758	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35.
|- (Tr A <-> A.x e. A x (_ A)
Theorem	dftr4 2759	An alternate way of defining a transitive class. Definition of [Enderton] p. 71.
|- (Tr A <-> A (_ P~A)
Theorem	treq 2760	Equality theorem for the transitive class predicate.
|- (A = B -> (Tr A <-> Tr B))
Theorem	trel 2761	In a transitive class, the membership relation is transitive.
|- (Tr A -> ((B e. C /\ C e. A) -> B e. A))
Theorem	trel3 2762	In a transitive class, the membership relation is transitive.
|- (Tr A -> ((B e. C /\ C e. D /\ D e. A) -> B e. A))
Theorem	trss 2763	An element of a transitive class is a subset of the class.
|- (Tr A -> (B e. A -> B (_ A))
Theorem	trin 2764	The intersection of transitive classes is transitive.
|- ((Tr A /\ Tr B) -> Tr (A i^i B))
Theorem	tr0 2765	The empty set is transitive.
|- Tr (/)
Theorem	trv 2766	The universe is transitive.
|- Tr V
ZF Set Theory - add the Axiom of Replacement
Introduce the Axiom of Replacement
Axiom	ax-rep 2767	Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory. Axiom 5 of [TakeutiZaring] p. 19. It tells us that that the image of any set under a function is also a set (see the variant funimaex 3682). Although ph may be any wff whatsoever, this axiom is useful (i.e. its antecedent is satisfied) when we are given some function and ph encodes the predicate "the value of the function at w is z". Thus ph will ordinarily have free variables w and z - think of it informally as ph(w, z). We prefix ph with the quantifier A.y in order to "protect" the axiom from any ph containing y, thus allowing us to eliminate any restrictions on ph. This makes the axiom usable in a formalization that omits the logically redundant axiom ax-17 1007. Another common variant is derived as axrep5 2772, where you can find some further remarks. A slightly more compact version is shown as axrep2 2769. A quite different variant is zfrep6 3721, which if used in place of ax-rep 2767 would also require that the Separation Scheme axsep 2776 be stated as a separate axiom. There is very a strong generalization of Replacement that doesn't demand function-like behavior of ph. Two versions of this generalization are called the Collection Principle cp 4868 and the Boundedness Axiom bnd 4869. Many developments of set theory distinguish the uses of Replacement from uses the weaker axioms of Separation axsep 2776, Null Set axnul 2783, and Pairing axpr 2854, all of which we derive from Replacement. In order to make it easier to identify the uses of those redundant axioms, we restate them as axioms ax-sep 2777, ax-nul 2784, and ax-pr 2855 below the theorems that prove them.
|- (A.wE.yA.z(A.yph -> z = y) -> E.yA.z(z e. y <-> E.w(w e. x /\ A.yph)))
Theorem	axrep1 2768	The version of the Axiom of Replacement used in the Metamath Solitaire applet http://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 2767 -> axrep1 2768 -> axrep2 2769 -> axrepnd 5100 -> zfcndrep 5120 = ax-rep 2767.
|- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ ph)))
Theorem	axrep2 2769	Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on ph.
|- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. y /\ A.yph)))
Theorem	axrep3 2770	Axiom of Replacement slightly strengthened from axrep2 2769; w may occur free in ph.
|- E.x(E.yA.z(ph -> z = y) -> A.z(z e. x <-> E.x(x e. w /\ A.yph)))
Theorem	axrep4 2771	A more traditional version of the Axiom of Replacement.
|- (ph -> A.zph)   =>   |- (A.xE.zA.y(ph -> y = z) -> E.zA.y(y e. z <-> E.x(x e. w /\ ph)))
Theorem	axrep5 2772	Axiom of Replacement (similar to Axiom Rep of [BellMachover] p. 463). The antecedent tells us ph is analogous to a "function" from x to y (although it is not really a function since it is a wff and not a class). In the consequent we postulate the existence of a set z that corresponds to the "image" of ph restricted to some other set w. The hypothesis says z must not be free in ph.
|- (ph -> A.zph)   =>   |- (A.x(x e. w -> E.zA.y(ph -> y = z)) -> E.zA.y(y e. z <-> E.x(x e. w /\ ph)))
Theorem	zfrepclf 2773	An inference rule based on the Axiom of Replacement. Typically, ph defines a function from x to y.
|- (w e. A -> A.x w e. A)   &   |- A e. V   &   |- (x e. A -> E.zA.y(ph -> y = z))   =>   |- E.zA.y(y e. z <-> E.x(x e. A /\ ph))
Theorem	zfrep3cl 2774	An inference rule based on the Axiom of Replacement. Typically, ph defines a function from x to y.
|- A e. V   &   |- (x e. A -> E.zA.y(ph -> y = z))   =>   |- E.zA.y(y e. z <-> E.x(x e. A /\ ph))
Theorem	zfrep4 2775	A version of Replacement using class abstractions.
|- {x | ph} e. V   &   |- (ph -> E.zA.y(ps -> y = z))   =>   |- {y | E.x(ph /\ ps)} e. V
Derive the Axiom of Separation
Theorem	axsep 2776	Separation Scheme, which is an axiom scheme of Zermelo's original theory. Scheme Sep of [BellMachover] p. 463. As we show here, it is redundant if we assume Replacement in the form of ax-rep 2767. Some textbooks present Separation as a separate axiom scheme in order to show that much of set theory can be derived without the stronger Replacement. The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x e. z) so that it asserts the existence of a collection only if it is smaller than some other collection z that already exists. This prevents Russell's paradox ru 1984. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. The variable x can appear free in the wff ph, which in textbooks is often written ph(x). To specify this in the Metamath language, we omit the distinct variable requirement ($d) that x not appear in ph. For a version using a class variable, see zfauscl 2779, which requires the Axiom of Extensionality as well as Replacement for its derivation. If we omit the requirement that y not occur in ph, we can derive a contradiction, as notzfaus 2815 shows (contradicting zfauscl 2779). However, as axsep2 2778 shows, we can eliminate the restriction that z not occur in ph. Note: the distinct variable restriction that z not occur in ph is actually redundant in this particular proof, but we keep it since its purpose is to demonstrate the derivation of the exact ax-sep 2777 from ax-rep 2767. This theorem should not be referenced by any proof. Instead, use ax-sep 2777 below so that the uses of the Axiom of Separation can be more easily identified.
|- E.yA.x(x e. y <-> (x e. z /\ ph))
Axiom	ax-sep 2777	The Axiom of Separation of ZF set theory. It was derived as axsep 2776 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.
|- E.yA.x(x e. y <-> (x e. z /\ ph))
Theorem	axsep2 2778	A less restrictive version of the Separation Scheme axsep 2776, where variables x and z can both appear free in the wff ph, which can therefore be thought of as ph(x, z). This version was derived from the more restrictive ax-sep 2777 with no additional set theory axioms.
|- E.yA.x(x e. y <-> (x e. z /\ ph))
Theorem	zfauscl 2779	Separation Scheme using a class variable. To derive this from ax-sep 2777, we invoke the Axiom of Extensionality (indirectly via vtocl 1888), which is needed for the justification of class variable notation. If we omit the requirement that y not occur in ph, we can derive a contradiction, as notzfaus 2815 shows.
|- A e. V   =>   |- E.yA.x(x e. y <-> (x e. A /\ ph))
Theorem	bm1.3ii 2780	Convert implication to equivalence using Aussonderung. Similar to Theorem 1.3ii of [BellMachover] p. 463.
|- E.xA.y(ph -> y e. x)   =>   |- E.xA.y(y e. x <-> ph)
Derive the Null Set Axiom
Theorem	zfnuleu 2781	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 1504 to strengthen axnul 2783).
|- E.xA.y -. y e. x   =>   |- E!xA.y -. y e. x
Theorem	axnul2 2782	Prove axnul 2783 directly from ax-rep 2767 without using any equality axioms (ax-9 1001 thru ax-16 1247). The wff x = x substituted for ph in the ax-rep 2767 instance is arbitrary. Here, we don't need to know if x = x is true or false, only that it's not both. (Contributed by Jeff Hoffman, 4-Feb-2008.)
|- E.xA.y -. y e. x
Theorem	axnul 2783	The Null Set Axiom of ZF set theory: there exists a set with no elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks, this is presented as a separate axiom; here we show it can be derived from Separation ax-sep 2777. This version of the Null Set Axiom tells us that at least one empty set exists, but does not tells us that it is unique - we need the Axiom of Extensionality to do that (see zfnuleu 2781). This proof, suggested by Jeff Hoffman (3-Feb-2008), does not require the set existence axiom ax-9 1001, unlike some empty set existence proofs (such as the remark in [Kunen] p. 11). However, it uses ax-4 1009, which also presupposes the existence of at least one set, i.e it does not hold in a "free logic" valid in empty domains. Theorem ax4 1008, which shows the redundancy of ax-4 1009, depends on ax-9 1001 for its proof. See axnul2 2782 for a similar proof directly from ax-rep 2767. This theorem should not be referenced by any proof. Instead, use ax-nul 2784 below so that the uses of the Null Set Axiom can be more easily identified.
|- E.xA.y -. y e. x
Axiom	ax-nul 2784	The Null Set Axiom of ZF set theory. It was derived as axnul 2783 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.
|- E.xA.y -. y e. x
Theorem	0ex 2785	The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 2784.
|- (/) e. V
Theorems requiring subset and intersection existence
Theorem	nalset 2786	No set contains all sets. Theorem 41 of [Suppes] p. 30.
|- -. E.xA.y y e. x
Theorem	vprc 2787	The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity.
|- -. V e. V
Theorem	nvel 2788	The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.)
|- -. V e. A
Theorem	vnex 2789	The universal class does not exist.
|- -. E.x x = V
Theorem	inex1 2790	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22.
|- A e. V   =>   |- (A i^i B) e. V
Theorem	inex2 2791	Separation Scheme (Aussonderung) using class notation.
|- A e. V   =>   |- (B i^i A) e. V
Theorem	inex1g 2792	Closed-form, generalized Separation Scheme.
|- (A e. C -> (A i^i B) e. V)
Theorem	ssex 2793	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 2777 (a.k.a. Subset Axiom).
|- B e. V   =>   |- (A (_ B -> A e. V)
Theorem	ssexi 2794	The subset of a set is also a set.
|- B e. V   &   |- A (_ B   =>   |- A e. V
Theorem	ssexg 2795	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized).
|- ((A (_ B /\ B e. C) -> A e. V)
Theorem	difexg 2796	Existence of a difference.
|- (A e. C -> (A \ B) e. V)
Theorem	zfausab 2797	Separation Scheme in terms of a class abstraction.
|- A e. V   =>   |- {x | (x e. A /\ ph)} e. V
Theorem	rabexg 2798	Separation Scheme in terms of a restricted class abstraction.
|- (A e. B -> {x e. A | ph} e. V)
Theorem	rabex 2799	Separation Scheme in terms of a restricted class abstraction.
|- A e. V   =>   |- {x e. A | ph} e. V
Theorem	elssabg 2800	Membership in a class abstraction involving a subset. Unlike elabg 1945, A does not have to be a set.
|- (x = A -> (ph <-> ps))   =>   |- (B e. C -> (A e. {x | (x (_ B /\ ph)} <-> (A (_ B /\ ps)))