P. 42 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brne0 4101	If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4102. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
|- ( A R B -> R =/= (/) )
Theorem	brm 4102*	If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
|- ( A R B -> E. x x e. R )
Theorem	brun 4103	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|- ( A ( R u. S ) B <-> ( A R B \/ A S B ) )
Theorem	brin 4104	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|- ( A ( R i^i S ) B <-> ( A R B /\ A S B ) )
Theorem	brdif 4105	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
|- ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )
Theorem	sbcbrg 4106	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C ) )
Theorem	sbcbr12g 4107*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R [_ A / x ]_ C ) )
Theorem	sbcbr1g 4108*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R C ) )
Theorem	sbcbr2g 4109*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> B R [_ A / x ]_ C ) )
Theorem	brralrspcev 4110*	Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
|- ( ( B e. X /\ A. y e. Y A R B ) -> E. x e. X A. y e. Y A R x )
Theorem	brimralrspcev 4111*	Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.)
|- ( ( B e. X /\ A. y e. Y ( ( ph /\ A R B ) -> ps ) ) -> E. x e. X A. y e. Y ( ( ph /\ A R x ) -> ps ) )
2.1.23  Ordered-pair class abstractions (class builders)
Syntax	copab 4112	Extend class notation to include ordered-pair class abstraction (class builder).
class { <. x , y >. | ph }
Syntax	cmpt 4113	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class ( x e. A |-> B )
Definition	df-opab 4114*	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. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)
|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
Definition	df-mpt 4115*	Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from x (in A) to B ( x )". The class expression B is the value of the function at x and normally contains the variable x. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
Theorem	opabss 4116*	The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- { <. x , y >. | x R y } C_ R
Theorem	opabbid 4117	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )
Theorem	opabbidv 4118*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )
Theorem	opabbii 4119	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
|- ( ph <-> ps )   =>    |- { <. x , y >. | ph } = { <. x , y >. | ps }
Theorem	nfopab 4120*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.)
|- F/ z ph   =>    |- F/_ z { <. x , y >. | ph }
Theorem	nfopab1 4121	The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { <. x , y >. | ph }
Theorem	nfopab2 4122	The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ y { <. x , y >. | ph }
Theorem	cbvopab 4123*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopabv 4124*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopab1 4125*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/ z ph   &    |- F/ x ps   &    |- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2 4126*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
|- F/ z ph   &    |- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	cbvopab1s 4127*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
|- { <. x , y >. | ph } = { <. z , y >. | [ z / x ] ph }
Theorem	cbvopab1v 4128*	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2v 4129*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
|- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	csbopabg 4130*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- ( A e. V -> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } )
Theorem	unopab 4131	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <. x , y >. | ph } u. { <. x , y >. | ps } ) = { <. x , y >. | ( ph \/ ps ) }
Theorem	mpteq12f 4132	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12dva 4133*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> A = C )   &    |- ( ( ph /\ x e. A ) -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12dv 4134*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12 4135*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
|- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq1 4136*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mpteq1d 4137*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mpteq2ia 4138	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ( x e. A -> B = C )   =>    |- ( x e. A |-> B ) = ( x e. A |-> C )
Theorem	mpteq2i 4139	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- B = C   =>    |- ( x e. A |-> B ) = ( x e. A |-> C )
Theorem	mpteq12i 4140	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- A = C   &    |- B = D   =>    |- ( x e. A |-> B ) = ( x e. C |-> D )
Theorem	mpteq2da 4141	Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	mpteq2dva 4142*	Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	mpteq2dv 4143*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
|- ( ph -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	nfmpt 4144*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( y e. A |-> B )
Theorem	nfmpt1 4145	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
|- F/_ x ( x e. A |-> B )
Theorem	cbvmptf 4146*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Thierry Arnoux, 9-Mar-2017.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmpt 4147*	Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmptv 4148*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	mptv 4149*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
|- ( x e. _V |-> B ) = { <. x , y >. | y = B }
2.1.24  Transitive classes
Syntax	wtr 4150	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr A
Definition	df-tr 4151	Define the transitive class predicate. Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4152 (which is suggestive of the word "transitive"), dftr3 4154, dftr4 4155, and dftr5 4153. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> U. A C_ A )
Theorem	dftr2 4152*	An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.)
|- ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
Theorem	dftr5 4153*	An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.)
|- ( Tr A <-> A. x e. A A. y e. x y e. A )
Theorem	dftr3 4154*	An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> A. x e. A x C_ A )
Theorem	dftr4 4155	An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.)
|- ( Tr A <-> A C_ ~P A )
Theorem	treq 4156	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
|- ( A = B -> ( Tr A <-> Tr B ) )
Theorem	trel 4157	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )
Theorem	trel3 4158	In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.)
|- ( Tr A -> ( ( B e. C /\ C e. D /\ D e. A ) -> B e. A ) )
Theorem	trss 4159	An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.)
|- ( Tr A -> ( B e. A -> B C_ A ) )
Theorem	trin 4160	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
|- ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )
Theorem	tr0 4161	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
|- Tr (/)
Theorem	trv 4162	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
|- Tr _V
Theorem	triun 4163*	The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( A. x e. A Tr B -> Tr U_ x e. A B )
Theorem	truni 4164*	The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
|- ( A. x e. A Tr x -> Tr U. A )
Theorem	trint 4165*	The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.)
|- ( A. x e. A Tr x -> Tr |^| A )
Theorem	trintssm 4166*	Any inhabited transitive class includes its intersection. Similar to Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the inhabitedness hypothesis). (Contributed by Jim Kingdon, 22-Aug-2018.)
|- ( ( Tr A /\ E. x x e. A ) -> |^| A C_ A )
2.2  IZF Set Theory - add the Axioms of Collection and Separation
2.2.1  Introduce the Axiom of Collection
Axiom	ax-coll 4167*	Axiom of Collection. Axiom 7 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). It is similar to bnd 4224 but uses a freeness hypothesis in place of one of the distinct variable conditions. (Contributed by Jim Kingdon, 23-Aug-2018.)
|- F/ b ph   =>    |- ( A. x e. a E. y ph -> E. b A. x e. a E. y e. b ph )
Theorem	repizf 4168*	Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 4167. It is identical to zfrep6 4169 except for the choice of a freeness hypothesis rather than a disjoint variable condition between b and ph. (Contributed by Jim Kingdon, 23-Aug-2018.)
|- F/ b ph   =>    |- ( A. x e. a E! y ph -> E. b A. x e. a E. y e. b ph )
Theorem	zfrep6 4169*	A version of the Axiom of Replacement. Normally ph would have free variables x and y. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4170 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version. (Contributed by NM, 10-Oct-2003.)
|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )
2.2.2  Introduce the Axiom of Separation
Axiom	ax-sep 4170*	The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed, and with a F/ y ph condition replaced by a disjoint variable condition between y and ph). 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 3001. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Theorem	axsep2 4171*	A less restrictive version of the Separation Scheme ax-sep 4170, 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 4170 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Theorem	zfauscl 4172*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4170, we invoke the Axiom of Extensionality (indirectly via vtocl 2829), which is needed for the justification of class variable notation. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
Theorem	bm1.3ii 4173*	Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4170. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.)
|- E. x A. y ( ph -> y e. x )   =>    |- E. x A. y ( y e. x <-> ph )
Theorem	a9evsep 4174*	Derive a weakened version of ax-i9 1554, where x and y must be distinct, from Separation ax-sep 4170 and Extensionality ax-ext 2188. The theorem -. A. x -. x = y also holds (ax9vsep 4175), but in intuitionistic logic E. x x = y is stronger. (Contributed by Jim Kingdon, 25-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E. x x = y
Theorem	ax9vsep 4175*	Derive a weakened version of ax-9 1555, where x and y must be distinct, from Separation ax-sep 4170 and Extensionality ax-ext 2188. In intuitionistic logic a9evsep 4174 is stronger and also holds. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. A. x -. x = y
2.2.3  Derive the Null Set Axiom
Theorem	zfnuleu 4176*	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2191 to strengthen the hypothesis in the form of axnul 4177). (Contributed by NM, 22-Dec-2007.)
|- E. x A. y -. y e. x   =>    |- E! x A. y -. y e. x
Theorem	axnul 4177*	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 4170. This version of the Null Set Axiom tells us that at least one empty set exists, but does not tell us that it is unique - we need the Axiom of Extensionality to do that (see zfnuleu 4176). This theorem should not be referenced by any proof. Instead, use ax-nul 4178 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E. x A. y -. y e. x
Axiom	ax-nul 4178*	The Null Set Axiom of IZF set theory. It was derived as axnul 4177 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by NM, 7-Aug-2003.)
|- E. x A. y -. y e. x
Theorem	0ex 4179	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 4178. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (/) e. _V
Theorem	csbexga 4180	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
|- ( ( A e. V /\ A. x B e. W ) -> [_ A / x ]_ B e. _V )
Theorem	csbexa 4181	The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   &    |- B e. _V   =>    |- [_ A / x ]_ B e. _V
2.2.4  Theorems requiring subset and intersection existence
Theorem	nalset 4182*	No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.)
|- -. E. x A. y y e. x
Theorem	vnex 4183	The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005.)
|- -. E. x x = _V
Theorem	vprc 4184	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. (Contributed by NM, 23-Aug-1993.)
|- -. _V e. _V
Theorem	nvel 4185	The universal class does not belong to any class. (Contributed by FL, 31-Dec-2006.)
|- -. _V e. A
Theorem	inex1 4186	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- ( A i^i B ) e. _V
Theorem	inex2 4187	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
|- A e. _V   =>    |- ( B i^i A ) e. _V
Theorem	inex1g 4188	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
|- ( A e. V -> ( A i^i B ) e. _V )
Theorem	ssex 4189	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 4170 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
|- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	ssexi 4190	The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
|- B e. _V   &    |- A C_ B   =>    |- A e. _V
Theorem	ssexg 4191	The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
|- ( ( A C_ B /\ B e. C ) -> A e. _V )
Theorem	ssexd 4192	A subclass of a set is a set. Deduction form of ssexg 4191. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> B e. C )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A e. _V )
Theorem	difexg 4193	Existence of a difference. (Contributed by NM, 26-May-1998.)
|- ( A e. V -> ( A \ B ) e. _V )
Theorem	zfausab 4194*	Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.)
|- A e. _V   =>    |- { x | ( x e. A /\ ph ) } e. _V
Theorem	rabexg 4195*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)
|- ( A e. V -> { x e. A | ph } e. _V )
Theorem	rabex 4196*	Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
|- A e. _V   =>    |- { x e. A | ph } e. _V
Theorem	rabexd 4197*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4198. (Contributed by AV, 16-Jul-2019.)
|- B = { x e. A | ps }   &    |- ( ph -> A e. V )   =>    |- ( ph -> B e. _V )
Theorem	rabex2 4198*	Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
|- B = { x e. A | ps }   &    |- A e. _V   =>    |- B e. _V
Theorem	rab2ex 4199*	A class abstraction based on a class abstraction based on a set is a set. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
|- B = { y e. A | ps }   &    |- A e. _V   =>    |- { x e. B | ph } e. _V
Theorem	elssabg 4200*	Membership in a class abstraction involving a subset. Unlike elabg 2923, A does not have to be a set. (Contributed by NM, 29-Aug-2006.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( B e. V -> ( A e. { x | ( x C_ B /\ ph ) } <-> ( A C_ B /\ ps ) ) )