P. 49 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4801-4900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inex1g 4801	Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
|- ( A e. V -> ( A i^i B ) e. _V )
Theorem	ssex 4802	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 4781 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
|- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	ssexi 4803	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 4804	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 4805	A subclass of a set is a set. Deduction form of ssexg 4804. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> B e. C )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A e. _V )
Theorem	prcssprc 4806	The superclass of a proper class is a proper class. (Contributed by AV, 27-Dec-2020.)
|- ( ( A C_ B /\ A e/ _V ) -> B e/ _V )
Theorem	sselpwd 4807	Elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)
|- ( ph -> B e. V )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A e. ~P B )
Theorem	difexg 4808	Existence of a difference. (Contributed by NM, 26-May-1998.)
|- ( A e. V -> ( A \ B ) e. _V )
Theorem	difexi 4809	Existence of a difference, inference version of difexg 4808. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Revised by AV, 26-Mar-2021.)
|- A e. _V   =>    |- ( A \ B ) e. _V
Theorem	difexOLD 4810	Obsolete version of difexi 4809 as of 26-Mar-2021. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A e. V   =>    |- ( A \ B ) e. _V
Theorem	zfausab 4811*	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 4812*	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 4813*	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 4814*	Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4815. (Contributed by AV, 16-Jul-2019.)
|- B = { x e. A | ps }   &    |- ( ph -> A e. V )   =>    |- ( ph -> B e. _V )
Theorem	rabex2 4815*	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 4816*	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	rabex2OLD 4817*	Obsolete version of rabex2 4815 as of 26-Mar-2021. (Contributed by AV, 16-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- B = { x e. A | ps }   &    |- A e. V   =>    |- B e. _V
Theorem	rab2exOLD 4818*	Obsolete version of rab2ex 4816 as of 26-Mar-2021. (Contributed by AV, 16-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- B = { y e. A | ps }   &    |- A e. V   =>    |- { x e. B | ph } e. _V
Theorem	elssabg 4819*	Membership in a class abstraction involving a subset. Unlike elabg 3351, 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 ) ) )
Theorem	intex 4820	The intersection of a nonempty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.)
|- ( A =/= (/) <-> |^| A e. _V )
Theorem	intnex 4821	If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005.)
|- ( -. |^| A e. _V <-> |^| A = _V )
Theorem	intexab 4822	The intersection of a nonempty class abstraction exists. (Contributed by NM, 21-Oct-2003.)
|- ( E. x ph <-> |^| { x | ph } e. _V )
Theorem	intexrab 4823	The intersection of a nonempty restricted class abstraction exists. (Contributed by NM, 21-Oct-2003.)
|- ( E. x e. A ph <-> |^| { x e. A | ph } e. _V )
Theorem	iinexg 4824*	The existence of a class intersection. x is normally a free-variable parameter in B, which should be read B ( x ). (Contributed by FL, 19-Sep-2011.)
|- ( ( A =/= (/) /\ A. x e. A B e. C ) -> |^|_ x e. A B e. _V )
Theorem	intabs 4825*	Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = |^| { y | ps } -> ( ph <-> ch ) )   &    |- ( |^| { y | ps } C_ A /\ ch )   =>    |- |^| { x | ( x C_ A /\ ph ) } = |^| { x | ph }
Theorem	inuni 4826*	The intersection of a union U. A with a class B is equal to the union of the intersections of each element of A with B. (Contributed by FL, 24-Mar-2007.)
|- ( U. A i^i B ) = U. { x | E. y e. A x = ( y i^i B ) }
Theorem	elpw2g 4827	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)
|- ( B e. V -> ( A e. ~P B <-> A C_ B ) )
Theorem	elpw2 4828	Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.)
|- B e. _V   =>    |- ( A e. ~P B <-> A C_ B )
Theorem	elpwi2 4829	Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- B e. V   &    |- A C_ B   =>    |- A e. ~P B
Theorem	pwnss 4830	The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( A e. V -> -. ~P A C_ A )
Theorem	pwne 4831	No set equals its power set. The sethood antecedent is necessary; compare pwv 4433. (Contributed by NM, 17-Nov-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- ( A e. V -> ~P A =/= A )
2.2.5  Theorems requiring empty set existence
Theorem	class2set 4832*	Construct, from any class A, a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists. (Contributed by NM, 16-Oct-2003.)
|- { x e. A | A e. _V } e. _V
Theorem	class2seteq 4833*	Equality theorem based on class2set 4832. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.)
|- ( A e. V -> { x e. A | A e. _V } = A )
Theorem	0elpw 4834	Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
|- (/) e. ~P A
Theorem	pwne0 4835	A power class is never empty. (Contributed by NM, 3-Sep-2018.)
|- ~P A =/= (/)
Theorem	0nep0 4836	The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.)
|- (/) =/= { (/) }
Theorem	0inp0 4837	Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 21-Jun-1993.)
|- ( A = (/) -> -. A = { (/) } )
Theorem	unidif0 4838	The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.)
|- U. ( A \ { (/) } ) = U. A
Theorem	iin0 4839*	An indexed intersection of the empty set, with a nonempty index set, is empty. (Contributed by NM, 20-Oct-2005.)
|- ( A =/= (/) <-> |^|_ x e. A (/) = (/) )
Theorem	notzfaus 4840*	In the Separation Scheme zfauscl 4783, we require that y not occur in ph (which can be generalized to "not be free in"). Here we show special cases of A and ph that result in a contradiction by violating this requirement. (Contributed by NM, 8-Feb-2006.)
|- A = { (/) }   &    |- ( ph <-> -. x e. y )   =>    |- -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) )
Theorem	intv 4841	The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.)
|- |^| _V = (/)
Theorem	axpweq 4842*	Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4843 is not used by the proof. (Contributed by NM, 22-Jun-2009.)
|- A e. _V   =>    |- ( ~P A e. _V <-> E. x A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) )
2.3  ZF Set Theory - add the Axiom of Power Sets
2.3.1  Introduce the Axiom of Power Sets
Axiom	ax-pow 4843*	Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. It states that a set y exists that includes the power set of a given set x i.e. contains every subset of x. The variant axpow2 4845 uses explicit subset notation. A version using class notation is pwex 4848. (Contributed by NM, 21-Jun-1993.)
|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
Theorem	zfpow 4844*	Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
|- E. x A. y ( A. x ( x e. y -> x e. z ) -> y e. x )
Theorem	axpow2 4845*	A variant of the Axiom of Power Sets ax-pow 4843 using subset notation. Problem in [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
|- E. y A. z ( z C_ x -> z e. y )
Theorem	axpow3 4846*	A variant of the Axiom of Power Sets ax-pow 4843. For any set x, there exists a set y whose members are exactly the subsets of x i.e. the power set of x. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
|- E. y A. z ( z C_ x <-> z e. y )
Theorem	el 4847*	Every set is an element of some other set. See elALT 4910 for a shorter proof using more axioms. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- E. y x e. y
Theorem	pwex 4848	Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- A e. _V   =>    |- ~P A e. _V
Theorem	vpwex 4849	The powerset of a setvar is a set. (Contributed by BJ, 3-May-2021.)
|- ~P x e. _V
Theorem	pwexg 4850	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.)
|- ( A e. V -> ~P A e. _V )
Theorem	abssexg 4851*	Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A e. V -> { x | ( x C_ A /\ ph ) } e. _V )
Theorem	snexALT 4852	Alternate proof of snex 4908 using Power Set (ax-pow 4843) instead of Pairing (ax-pr 4906). Unlike in the proof of zfpair 4904, Replacement (ax-rep 4771) is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { A } e. _V
Theorem	p0ex 4853	The power set of the empty set (the ordinal 1) is a set. See also p0exALT 4854. (Contributed by NM, 23-Dec-1993.)
|- { (/) } e. _V
Theorem	p0exALT 4854	Alternate proof of p0ex 4853 which is quite different and longer if snexALT 4852 is expanded. (Contributed by NM, 23-Dec-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { (/) } e. _V
Theorem	pp0ex 4855	The power set of the power set of the empty set (the ordinal 2) is a set. (Contributed by NM, 24-Jun-1993.)
|- { (/) , { (/) } } e. _V
Theorem	ord3ex 4856	The ordinal number 3 is a set, proved without the Axiom of Union ax-un 6949. (Contributed by NM, 2-May-2009.)
|- { (/) , { (/) } , { (/) , { (/) } } } e. _V
Theorem	dtru 4857*	At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Note that we may not substitute the same variable for both x and y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 1957. This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2602 or ax-sep 4781. See dtruALT 4899 for a shorter proof using these axioms. The proof makes use of dummy variables z and w which do not appear in the final theorem. They must be distinct from each other and from x and y. In other words, if we were to substitute x for z throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006.)
|- -. A. x x = y
Theorem	axc16b 4858*	This theorem shows that axiom ax-c16 34177 is redundant in the presence of theorem dtru 4857, which states simply that at least two things exist. This justifies the remark at mmzfcnd.html#twoness (which links to this theorem). (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 7-Nov-2006.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	eunex 4859	Existential uniqueness implies there is a value for which the wff argument is false. (Contributed by NM, 24-Oct-2010.)
|- ( E! x ph -> E. x -. ph )
Theorem	eusv1 4860*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by NM, 14-Oct-2010.)
|- ( E! y A. x y = A <-> E. y A. x y = A )
Theorem	eusvnf 4861*	Even if x is free in A, it is effectively bound when A ( x ) is single-valued. (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- ( E! y A. x y = A -> F/_ x A )
Theorem	eusvnfb 4862*	Two ways to say that A ( x ) is a set expression that does not depend on x. (Contributed by Mario Carneiro, 18-Nov-2016.)
|- ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) )
Theorem	eusv2i 4863*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.)
|- ( E! y A. x y = A -> E! y E. x y = A )
Theorem	eusv2nf 4864*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by Mario Carneiro, 18-Nov-2016.)
|- A e. _V   =>    |- ( E! y E. x y = A <-> F/_ x A )
Theorem	eusv2 4865*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by NM, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- A e. _V   =>    |- ( E! y E. x y = A <-> E! y A. x y = A )
Theorem	reusv1 4866*	Two ways to express single-valuedness of a class expression C ( y ). (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.)
|- ( E. y e. B ph -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )
Theorem	reusv1OLD 4867*	Obsolete proof of reusv1 4866 as of 7-Aug-2021. (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( E. y e. B ph -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )
Theorem	reusv2lem1 4868*	Lemma for reusv2 4874. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( A =/= (/) -> ( E! x A. y e. A x = B <-> E. x A. y e. A x = B ) )
Theorem	reusv2lem2 4869*	Lemma for reusv2 4874. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.)
|- ( E! x A. y e. A x = B -> E! x E. y e. A x = B )
Theorem	reusv2lem2OLD 4870*	Obsolete proof of reusv2lem2 4869 as of 7-Aug-2021. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( E! x A. y e. A x = B -> E! x E. y e. A x = B )
Theorem	reusv2lem3 4871*	Lemma for reusv2 4874. (Contributed by NM, 14-Dec-2012.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( A. y e. A B e. _V -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) )
Theorem	reusv2lem4 4872*	Lemma for reusv2 4874. (Contributed by NM, 13-Dec-2012.)
|- ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x A. y e. B ( ( C e. A /\ ph ) -> x = C ) )
Theorem	reusv2lem5 4873*	Lemma for reusv2 4874. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( ( A. y e. B C e. A /\ B =/= (/) ) -> ( E! x e. A E. y e. B x = C <-> E! x e. A A. y e. B x = C ) )
Theorem	reusv2 4874*	Two ways to express single-valuedness of a class expression C ( y ) that is constant for those y e. B such that ph. The first antecedent ensures that the constant value belongs to the existential uniqueness domain A, and the second ensures that C ( y ) is evaluated for at least one y. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( ( A. y e. B ( ph -> C e. A ) /\ E. y e. B ph ) -> ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x e. A A. y e. B ( ph -> x = C ) ) )
Theorem	reusv3i 4875*	Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.)
|- ( y = z -> ( ph <-> ps ) )   &    |- ( y = z -> C = D )   =>    |- ( E. x e. A A. y e. B ( ph -> x = C ) -> A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) )
Theorem	reusv3 4876*	Two ways to express single-valuedness of a class expression C ( y ). See reusv1 4866 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.)
|- ( y = z -> ( ph <-> ps ) )   &    |- ( y = z -> C = D )   =>    |- ( E. y e. B ( ph /\ C e. A ) -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )
Theorem	eusv4 4877*	Two ways to express single-valuedness of a class expression B ( x ). (Contributed by NM, 27-Oct-2010.)
|- B e. _V   =>    |- ( E! x E. y e. A x = B <-> E! x A. y e. A x = B )
Theorem	alxfr 4878*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 18-Feb-2007.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A. y A e. B /\ A. x E. y x = A ) -> ( A. x ph <-> A. y ps ) )
Theorem	ralxfrd 4879*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) )
Theorem	ralxfrdOLD 4880*	Obsolete proof of ralxfrd 4879 as of 7-Aug-2021. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) )
Theorem	rexxfrd 4881*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) )
Theorem	ralxfr2d 4882*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by Mario Carneiro, 20-Aug-2014.)
|- ( ( ph /\ y e. C ) -> A e. V )   &    |- ( ph -> ( x e. B <-> E. y e. C x = A ) )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) )
Theorem	rexxfr2d 4883*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( ( ph /\ y e. C ) -> A e. V )   &    |- ( ph -> ( x e. B <-> E. y e. C x = A ) )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) )
Theorem	ralxfrd2 4884*	Transfer universal quantification from a variable x to another variable y contained in expression A. Variant of ralxfrd 4879. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ y e. C /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) )
Theorem	rexxfrd2 4885*	Transfer existence from a variable x to another variable y contained in expression A. Variant of rexxfrd 4881. (Contributed by Alexander van der Vekens, 25-Apr-2018.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ y e. C /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) )
Theorem	ralxfr 4886*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
|- ( y e. C -> A e. B )   &    |- ( x e. B -> E. y e. C x = A )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x e. B ph <-> A. y e. C ps )
Theorem	ralxfrALT 4887*	Alternate proof of ralxfr 4886 which does not use ralxfrd 4879. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( y e. C -> A e. B )   &    |- ( x e. B -> E. y e. C x = A )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x e. B ph <-> A. y e. C ps )
Theorem	rexxfr 4888*	Transfer existence from a variable x to another variable y contained in expression A. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
|- ( y e. C -> A e. B )   &    |- ( x e. B -> E. y e. C x = A )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( E. x e. B ph <-> E. y e. C ps )
Theorem	rabxfrd 4889*	Class builder membership after substituting an expression A (containing y) for x in the class expression ch. (Contributed by NM, 16-Jan-2012.)
|- F/_ y B   &    |- F/_ y C   &    |- ( ( ph /\ y e. D ) -> A e. D )   &    |- ( x = A -> ( ps <-> ch ) )   &    |- ( y = B -> A = C )   =>    |- ( ( ph /\ B e. D ) -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) )
Theorem	rabxfr 4890*	Class builder membership after substituting an expression A (containing y) for x in the class expression ph. (Contributed by NM, 10-Jun-2005.)
|- F/_ y B   &    |- F/_ y C   &    |- ( y e. D -> A e. D )   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> A = C )   =>    |- ( B e. D -> ( C e. { x e. D | ph } <-> B e. { y e. D | ps } ) )
Theorem	reuxfr2d 4891*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. (Contributed by NM, 16-Jan-2012.) (Revised by NM, 16-Jun-2017.)
|- ( ( ph /\ y e. B ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E* y e. B x = A )   =>    |- ( ph -> ( E! x e. B E. y e. B ( x = A /\ ps ) <-> E! y e. B ps ) )
Theorem	reuxfr2 4892*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. (Contributed by NM, 14-Nov-2004.) (Revised by NM, 16-Jun-2017.)
|- ( y e. B -> A e. B )   &    |- ( x e. B -> E* y e. B x = A )   =>    |- ( E! x e. B E. y e. B ( x = A /\ ph ) <-> E! y e. B ph )
Theorem	reuxfrd 4893*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Use reuhypd 4895 to eliminate the second hypothesis. (Contributed by NM, 16-Jan-2012.)
|- ( ( ph /\ y e. B ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E! y e. B x = A )   &    |- ( x = A -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x e. B ps <-> E! y e. B ch ) )
Theorem	reuxfr 4894*	Transfer existential uniqueness from a variable x to another variable y contained in expression A. Use reuhyp 4896 to eliminate the second hypothesis. (Contributed by NM, 14-Nov-2004.)
|- ( y e. B -> A e. B )   &    |- ( x e. B -> E! y e. B x = A )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( E! x e. B ph <-> E! y e. B ps )
Theorem	reuhypd 4895*	A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd 6642. (Contributed by NM, 16-Jan-2012.)
|- ( ( ph /\ x e. C ) -> B e. C )   &    |- ( ( ph /\ x e. C /\ y e. C ) -> ( x = A <-> y = B ) )   =>    |- ( ( ph /\ x e. C ) -> E! y e. C x = A )
Theorem	reuhyp 4896*	A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr 4894. (Contributed by NM, 15-Nov-2004.)
|- ( x e. C -> B e. C )   &    |- ( ( x e. C /\ y e. C ) -> ( x = A <-> y = B ) )   =>    |- ( x e. C -> E! y e. C x = A )
Theorem	nfnid 4897	A setvar variable is not free from itself. The proof relies on dtru 4857, that is, it is not true in a one-element domain. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- -. F/_ x x
Theorem	nfcvb 4898	The "distinctor" expression -. A. x x = y, stating that x and y are not the same variable, can be written in terms of F/ in the obvious way. This theorem is not true in a one-element domain, because then F/_ x y and A. x x = y will both be true. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- ( F/_ x y <-> -. A. x x = y )
Theorem	dtruALT 4899*	Alternate proof of dtru 4857 which requires more axioms but is shorter and may be easier to understand. Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that x and y be distinct. Specifically, theorem spcev 3300 requires that x must not occur in the subexpression -. y = { (/) } in step 4 nor in the subexpression -. y = (/) in step 9. The proof verifier will require that x and y be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. (Contributed by NM, 15-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. A. x x = y
Theorem	dtrucor 4900*	Corollary of dtru 4857. This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 4901. (Contributed by NM, 27-Jun-2002.)
|- x = y   =>    |- x =/= y