P. 48 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4701-4800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	br0 4701	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
|- -. A (/) B
Theorem	brne0 4702	If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
|- ( A R B -> R =/= (/) )
Theorem	brun 4703	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 4704	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 4705	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
|- ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )
Theorem	sbcbr123 4706	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Modified by NM, 22-Aug-2018.)
|- ( [. A / x ]. B R C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C )
Theorem	sbcbr 4707*	Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018.)
|- ( [. A / x ]. B R C <-> B [_ A / x ]_ R C )
Theorem	sbcbr12g 4708*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. V -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R [_ A / x ]_ C ) )
Theorem	sbcbr1g 4709*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. V -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R C ) )
Theorem	sbcbr2g 4710*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. V -> ( [. A / x ]. B R C <-> B R [_ A / x ]_ C ) )
Theorem	brsymdif 4711	Characterization of the symmetric difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2012.)
|- ( A ( R /_\ S ) B <-> -. ( A R B <-> A S B ) )
2.1.23  Ordered-pair class abstractions (class builders)
Syntax	copab 4712	Extend class notation to include ordered-pair class abstraction (class builder).
class { <. x , y >. | ph }
Definition	df-opab 4713*	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 5027 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 7222. For example, R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 (ex-opab 27289). (Contributed by NM, 4-Jul-1994.)
|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
Theorem	opabss 4714*	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 4715	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (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 4716*	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )
Theorem	opabbii 4717	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
|- ( ph <-> ps )   =>    |- { <. x , y >. | ph } = { <. x , y >. | ps }
Theorem	nfopab 4718*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- F/ z ph   =>    |- F/_ z { <. x , y >. | ph }
Theorem	nfopab1 4719	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 4720	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 4721*	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 4722*	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 4723*	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 4724*	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 4725*	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 4726*	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 4727*	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	unopab 4728	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <. x , y >. | ph } u. { <. x , y >. | ps } ) = { <. x , y >. | ( ph \/ ps ) }
2.1.24  Functions in "maps-to" notation
Syntax	cmpt 4729	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-mpt 4730*	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. An example is the square function for complex numbers, ( x e. CC |-> ( x ^ 2 ) ). 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	mpteq12f 4731	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 4732*	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 4733*	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	mpteq12d 4734	An equality inference for the maps to notation. Compare mpteq12dv 4733. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/ x ph   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12df 4735	An equality theorem for the maps to notation. (Contributed by Thierry Arnoux, 30-May-2020.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x C   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12 4736*	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 4737*	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 4738*	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	mpteq1i 4739*	An equality theorem for the maps to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- A = B   =>    |- ( x e. A |-> C ) = ( x e. B |-> C )
Theorem	mpteq2ia 4740	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 4741	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 4742	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 4743	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 4744*	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 4745*	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 4746*	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 4747	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
|- F/_ x ( x e. A |-> B )
Theorem	cbvmptf 4748*	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 4749*	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 4750*	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 4751*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
|- ( x e. _V |-> B ) = { <. x , y >. | y = B }
2.1.25  Transitive classes
Syntax	wtr 4752	Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35.
wff Tr A
Definition	df-tr 4753	Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5508). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4754 (which is suggestive of the word "transitive"), dftr3 4756, dftr4 4757, dftr5 4755, and (when A is a set) unisuc 5801. 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 4754*	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 4755*	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 4756*	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 4757	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 4758	Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
|- ( A = B -> ( Tr A <-> Tr B ) )
Theorem	trel 4759	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 4760	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 4761	An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) (Proof shortened by JJ, 26-Jul-2021.)
|- ( Tr A -> ( B e. A -> B C_ A ) )
Theorem	trssOLD 4762	Obsolete proof of trss 4761 as of 26-Jul-2021. (Contributed by NM, 7-Aug-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( Tr A -> ( B e. A -> B C_ A ) )
Theorem	trin 4763	The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.)
|- ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )
Theorem	tr0 4764	The empty set is transitive. (Contributed by NM, 16-Sep-1993.)
|- Tr (/)
Theorem	trv 4765	The universe is transitive. (Contributed by NM, 14-Sep-2003.)
|- Tr _V
Theorem	triun 4766*	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 4767*	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 4768*	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	trintss 4769	Any nonempty transitive class includes its intersection. Exercise 3 in [TakeutiZaring] p. 44 (which mistakenly does not include the nonemptiness hypothesis). (Contributed by Scott Fenton, 3-Mar-2011.) (Proof shortened by Andrew Salmon, 14-Nov-2011.)
|- ( ( Tr A /\ A =/= (/) ) -> |^| A C_ A )
Theorem	trintssOLD 4770	Obsolete version of trintss 4769 as of 30-Oct-2021. (Contributed by Scott Fenton, 3-Mar-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A =/= (/) /\ Tr A ) -> |^| A C_ A )
2.2  ZF Set Theory - add the Axiom of Replacement
2.2.1  Introduce the Axiom of Replacement
Axiom	ax-rep 4771*	Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory. Axiom 5 of [TakeutiZaring] p. 19. It tells us that the image of any set under a function is also a set (see the variant funimaex 5976). 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. Another common variant is derived as axrep5 4776, where you can find some further remarks. A slightly more compact version is shown as axrep2 4773. A quite different variant is zfrep6 7134, which if used in place of ax-rep 4771 would also require that the Separation Scheme axsep 4780 be stated as a separate axiom. There is a very strong generalization of Replacement that doesn't demand function-like behavior of ph. Two versions of this generalization are called the Collection Principle cp 8754 and the Boundedness Axiom bnd 8755. Many developments of set theory distinguish the uses of Replacement from uses of the weaker axioms of Separation axsep 4780, Null Set axnul 4788, and Pairing axpr 4905, 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 4781, ax-nul 4789, and ax-pr 4906 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.)
|- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
Theorem	axrep1 4772*	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 4771 -> axrep1 4772 -> axrep2 4773 -> axrepnd 9416 -> zfcndrep 9436 = ax-rep 4771. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) )
Theorem	axrep2 4773*	Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on ph. (Contributed by NM, 15-Aug-2003.)
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) )
Theorem	axrep3 4774*	Axiom of Replacement slightly strengthened from axrep2 4773; w may occur free in ph. (Contributed by NM, 2-Jan-1997.)
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) )
Theorem	axrep4 4775*	A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994.)
|- F/ z ph   =>    |- ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
Theorem	axrep5 4776*	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. (Contributed by NM, 26-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/ z ph   =>    |- ( A. x ( x e. w -> E. z A. y ( ph -> y = z ) ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
Theorem	zfrepclf 4777*	An inference rule based on the Axiom of Replacement. Typically, ph defines a function from x to y. (Contributed by NM, 26-Nov-1995.)
|- F/_ x A   &    |- A e. _V   &    |- ( x e. A -> E. z A. y ( ph -> y = z ) )   =>    |- E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) )
Theorem	zfrep3cl 4778*	An inference rule based on the Axiom of Replacement. Typically, ph defines a function from x to y. (Contributed by NM, 26-Nov-1995.)
|- A e. _V   &    |- ( x e. A -> E. z A. y ( ph -> y = z ) )   =>    |- E. z A. y ( y e. z <-> E. x ( x e. A /\ ph ) )
Theorem	zfrep4 4779*	A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995.)
|- { x | ph } e. _V   &    |- ( ph -> E. z A. y ( ps -> y = z ) )   =>    |- { y | E. x ( ph /\ ps ) } e. _V
2.2.2  Derive the Axiom of Separation
Theorem	axsep 4780*	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 4771. 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 3434. 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 4783, which requires the Axiom of Extensionality as well as Separation for its derivation. If we omit the requirement that y not occur in ph, we can derive a contradiction, as notzfaus 4840 shows (contradicting zfauscl 4783). However, as axsep2 4782 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 4781 from ax-rep 4771. This theorem should not be referenced by any proof. Instead, use ax-sep 4781 below so that the uses of the Axiom of Separation can be more easily identified. (Contributed by NM, 11-Sep-2006.) (New usage is discouraged.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Axiom	ax-sep 4781*	The Axiom of Separation of ZF set theory. See axsep 4780 for more information. It was derived as axsep 4780 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 11-Sep-2006.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Theorem	axsep2 4782*	A less restrictive version of the Separation Scheme axsep 4780, 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 4781 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 4783*	Separation Scheme (Aussonderung) using a class variable. To derive this from ax-sep 4781, we invoke the Axiom of Extensionality (indirectly via vtocl 3259), 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 4840 shows. (Contributed by NM, 21-Jun-1993.)
|- A e. _V   =>    |- E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
Theorem	bm1.3ii 4784*	Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4781. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 21-Jun-1993.)
|- E. x A. y ( ph -> y e. x )   =>    |- E. x A. y ( y e. x <-> ph )
Theorem	ax6vsep 4785*	Derive ax6v 1889 (a weakened version of ax-6 1888 where x and y must be distinct), from Separation ax-sep 4781 and Extensionality ax-ext 2602. See ax6 2251 for the derivation of ax-6 1888 from ax6v 1889. (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 4786*	Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2607 to strengthen the hypothesis in the form of axnul 4788). (Contributed by NM, 22-Dec-2007.)
|- E. x A. y -. y e. x   =>    |- E! x A. y -. y e. x
Theorem	axnulALT 4787*	Alternate proof of axnul 4788, proved from propositional calculus, ax-gen 1722, ax-4 1737, sp 2053, and ax-rep 4771. To check this, replace sp 2053 with the obsolete axiom ax-c5 34168 in the proof of axnulALT 4787 and type the Metamath command 'SHOW TRACEBACK axnulALT / AXIOMS'. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E. x A. y -. y e. x
Theorem	axnul 4788*	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 4781. 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 4786). This proof, suggested by Jeff Hoffman, uses only ax-4 1737 and ax-gen 1722 from predicate calculus, which are valid in "free logic" i.e. logic holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc] p. 277). Thus, our ax-sep 4781 implies the existence of at least one set. Note that Kunen's version of ax-sep 4781 (Axiom 3 of [Kunen] p. 11) does not imply the existence of a set because his is universally closed i.e. prefixed with universal quantifiers to eliminate all free variables. His existence is provided by a separate axiom stating E. x x = x (Axiom 0 of [Kunen] p. 10). See axnulALT 4787 for a proof directly from ax-rep 4771. This theorem should not be referenced by any proof. Instead, use ax-nul 4789 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 4789*	The Null Set Axiom of ZF set theory. It was derived as axnul 4788 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 7-Aug-2003.)
|- E. x A. y -. y e. x
Theorem	0ex 4790	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 4789. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (/) e. _V
Theorem	sseliALT 4791	Alternate proof of sseli 3599 illustrating the use of the weak deduction theorem to prove it from the inference sselii 3600. (Contributed by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A C_ B   =>    |- ( C e. A -> C e. B )
Theorem	csbexg 4792	The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 17-Aug-2018.)
|- ( A. x B e. W -> [_ A / x ]_ B e. _V )
Theorem	csbex 4793	The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Revised by NM, 17-Aug-2018.)
|- B e. _V   =>    |- [_ A / x ]_ B e. _V
Theorem	unisn2 4794	A version of unisn 4451 without the A e. _V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006.)
|- U. { A } e. { (/) , A }
2.2.4  Theorems requiring subset and intersection existence
Theorem	nalset 4795*	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	vprc 4796	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 4797	The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.)
|- -. _V e. A
Theorem	vnex 4798	The universal class does not exist. (Contributed by NM, 4-Jul-2005.)
|- -. E. x x = _V
Theorem	inex1 4799	Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)
|- A e. _V   =>    |- ( A i^i B ) e. _V
Theorem	inex2 4800	Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)
|- A e. _V   =>    |- ( B i^i A ) e. _V