P. 40 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3901-4000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	difrab 3901	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
|- ( { x e. A | ph } \ { x e. A | ps } ) = { x e. A | ( ph /\ -. ps ) }
Theorem	dfrab3 3902*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- { x e. A | ph } = ( A i^i { x | ph } )
Theorem	dfrab2 3903*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.)
|- { x e. A | ph } = ( { x | ph } i^i A )
Theorem	notrab 3904*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A \ { x e. A | ph } ) = { x e. A | -. ph }
Theorem	dfrab3ss 3905*	Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 8-Nov-2015.)
|- ( A C_ B -> { x e. A | ph } = ( A i^i { x e. B | ph } ) )
Theorem	rabun2 3906	Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.)
|- { x e. ( A u. B ) | ph } = ( { x e. A | ph } u. { x e. B | ph } )
2.1.13.7  Restricted uniqueness with difference, union, and intersection
Theorem	reuss2 3907*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
|- ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> E! x e. A ph )
Theorem	reuss 3908*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
|- ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> E! x e. A ph )
Theorem	reuun1 3909*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
|- ( ( E. x e. A ph /\ E! x e. ( A u. B ) ( ph \/ ps ) ) -> E! x e. A ph )
Theorem	reuun2 3910*	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)
|- ( -. E. x e. B ph -> ( E! x e. ( A u. B ) ph <-> E! x e. A ph ) )
Theorem	reupick 3911*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
|- ( ( ( A C_ B /\ ( E. x e. A ph /\ E! x e. B ph ) ) /\ ph ) -> ( x e. A <-> x e. B ) )
Theorem	reupick3 3912*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
|- ( ( E! x e. A ph /\ E. x e. A ( ph /\ ps ) /\ x e. A ) -> ( ph -> ps ) )
Theorem	reupick2 3913*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( ( ( A. x e. A ( ps -> ph ) /\ E. x e. A ps /\ E! x e. A ph ) /\ x e. A ) -> ( ph <-> ps ) )
Theorem	euelss 3914*	Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.)
|- ( ( A C_ B /\ E. x x e. A /\ E! x x e. B ) -> E! x x e. A )
2.1.14  The empty set
Syntax	c0 3915	Extend class notation to include the empty set.
class (/)
Definition	df-nul 3916	Define the empty set. Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 3917. (Contributed by NM, 17-Jun-1993.)
|- (/) = ( _V \ _V )
Theorem	dfnul2 3917	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.)
|- (/) = { x | -. x = x }
Theorem	dfnul3 3918	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.)
|- (/) = { x e. A | -. x e. A }
Theorem	noel 3919	The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
|- -. A e. (/)
Theorem	n0i 3920	If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
|- ( B e. A -> -. A = (/) )
Theorem	ne0i 3921	If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
|- ( B e. A -> A =/= (/) )
Theorem	n0ii 3922	If a set has elements, then it is not empty. Inference associated with n0i 3920. (Contributed by BJ, 15-Jul-2021.)
|- A e. B   =>    |- -. B = (/)
Theorem	ne0ii 3923	If a set has elements, then it is not empty. Inference associated with ne0i 3921. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- A e. B   =>    |- B =/= (/)
Theorem	vn0 3924	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.)
|- _V =/= (/)
Theorem	eq0f 3925	The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by BJ, 15-Jul-2021.)
|- F/_ x A   =>    |- ( A = (/) <-> A. x -. x e. A )
Theorem	neq0f 3926	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of neq0 3930 requires only that x not be free in, rather than not occur in, A. (Contributed by BJ, 15-Jul-2021.)
|- F/_ x A   =>    |- ( -. A = (/) <-> E. x x e. A )
Theorem	n0f 3927	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 3931 requires only that x not be free in, rather than not occur in, A. (Contributed by NM, 17-Oct-2003.)
|- F/_ x A   =>    |- ( A =/= (/) <-> E. x x e. A )
Theorem	n0fOLD 3928	Obsolete proof of n0f 3927 as of 15-Jul-2021. (Contributed by NM, 17-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/_ x A   =>    |- ( A =/= (/) <-> E. x x e. A )
Theorem	eq0 3929*	The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.)
|- ( A = (/) <-> A. x -. x e. A )
Theorem	neq0 3930*	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.)
|- ( -. A = (/) <-> E. x x e. A )
Theorem	n0 3931*	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.)
|- ( A =/= (/) <-> E. x x e. A )
Theorem	nel0 3932*	From the general negation of membership in A, infer that A is the empty set. (Contributed by BJ, 6-Oct-2018.)
|- -. x e. A   =>    |- A = (/)
Theorem	reximdva0 3933*	Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.)
|- ( ( ph /\ x e. A ) -> ps )   =>    |- ( ( ph /\ A =/= (/) ) -> E. x e. A ps )
Theorem	rspn0 3934*	Specialization for restricted generalization with a nonempty set. (Contributed by Alexander van der Vekens, 6-Sep-2018.)
|- ( A =/= (/) -> ( A. x e. A ph -> ph ) )
Theorem	n0rex 3935*	There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.)
|- ( A =/= (/) -> E. x e. A x e. A )
Theorem	ssn0rex 3936*	There is an element in a class with a nonempty subclass which is an element of the subclass. (Contributed by AV, 17-Dec-2020.)
|- ( ( A C_ B /\ A =/= (/) ) -> E. x e. B x e. A )
Theorem	n0moeu 3937*	A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.)
|- ( A =/= (/) -> ( E* x x e. A <-> E! x x e. A ) )
Theorem	rex0 3938	Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.)
|- -. E. x e. (/) ph
Theorem	0el 3939*	Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.)
|- ( (/) e. A <-> E. x e. A A. y -. y e. x )
Theorem	n0el 3940*	Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.)
|- ( -. (/) e. A <-> A. x e. A E. u u e. x )
Theorem	eqeuel 3941*	A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022.)
|- ( ( A =/= (/) /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) -> E! x x e. A )
Theorem	ssdif0 3942	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
|- ( A C_ B <-> ( A \ B ) = (/) )
Theorem	difn0 3943	If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017.)
|- ( ( A \ B ) =/= (/) -> A =/= B )
Theorem	pssdifn0 3944	A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.)
|- ( ( A C_ B /\ A =/= B ) -> ( B \ A ) =/= (/) )
Theorem	pssdif 3945	A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- ( A C. B -> ( B \ A ) =/= (/) )
Theorem	difin0ss 3946	Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
|- ( ( ( A \ B ) i^i C ) = (/) -> ( C C_ A -> C C_ B ) )
Theorem	inssdif0 3947	Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
|- ( ( A i^i B ) C_ C <-> ( A i^i ( B \ C ) ) = (/) )
Theorem	difid 3948	The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.)
|- ( A \ A ) = (/)
Theorem	difidALT 3949	Alternate proof of difid 3948. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A \ A ) = (/)
Theorem	dif0 3950	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
|- ( A \ (/) ) = A
Theorem	ab0 3951	The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 3954 (from which it could be proved using as many essential proof steps but one fewer syntactic step, at the cost of depending on df-ne 2795). (Contributed by BJ, 19-Mar-2021.)
|- ( { x | ph } = (/) <-> A. x -. ph )
Theorem	dfnf5 3952	Characterization of non-freeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.)
|- ( F/ x ph <-> ( { x | ph } = (/) \/ { x | ph } = _V ) )
Theorem	ab0orv 3953*	The class builder of a wff not containing the abstraction variable is either the empty set or the universal class. (Contributed by Mario Carneiro, 29-Aug-2013.) (Revised by BJ, 22-Mar-2020.)
|- ( { x | ph } = (/) \/ { x | ph } = _V )
Theorem	abn0 3954	Nonempty class abstraction. See also ab0 3951. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|- ( { x | ph } =/= (/) <-> E. x ph )
Theorem	rab0 3955	Any restricted class abstraction restricted to the empty set is empty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.)
|- { x e. (/) | ph } = (/)
Theorem	rab0OLD 3956	Obsolete proof of rab0 3955 as of 14-Jul-2021. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. (/) | ph } = (/)
Theorem	rabeq0 3957	Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.)
|- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )
Theorem	rabn0 3958	Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)
|- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
Theorem	rabn0OLD 3959	Obsolete proof of rabn0 3958 as of 16-Jul-2021. (Contributed by NM, 29-Aug-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
Theorem	rabeq0OLD 3960	Obsolete proof of rabeq0 3957 as of 16-Jul-2021. (Contributed by Jeff Madsen, 7-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( { x e. A | ph } = (/) <-> A. x e. A -. ph )
Theorem	rabxm 3961*	Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- A = ( { x e. A | ph } u. { x e. A | -. ph } )
Theorem	rabnc 3962*	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- ( { x e. A | ph } i^i { x e. A | -. ph } ) = (/)
Theorem	elneldisj 3963*	The set of elements s determining classes C (which may depend on s) containing a special element and the set of elements s determining classes C not containing the special element are disjoint. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Revised by AV, 17-Dec-2021.)
|- E = { s e. A | B e. C }   &    |- N = { s e. A | B e/ C }   =>    |- ( E i^i N ) = (/)
Theorem	elnelun 3964*	The union of the set of elements s determining classes C (which may depend on s) containing a special element and the set of elements s determining classes C not containing the special element yields the original set. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Revised by AV, 17-Dec-2021.)
|- E = { s e. A | B e. C }   &    |- N = { s e. A | B e/ C }   =>    |- ( E u. N ) = A
Theorem	elneldisjOLD 3965*	Obsolete version of elneldisj 3963 as of 17-Dec-2021. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E = { s e. A | B e. s }   &    |- N = { s e. A | B e/ s }   =>    |- ( E i^i N ) = (/)
Theorem	elnelunOLD 3966*	Obsolete version of elnelun 3964 as of 17-Dec-2021. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E = { s e. A | B e. s }   &    |- N = { s e. A | B e/ s }   =>    |- ( E u. N ) = A
Theorem	un0 3967	The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 15-Jul-1993.)
|- ( A u. (/) ) = A
Theorem	in0 3968	The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 21-Jun-1993.)
|- ( A i^i (/) ) = (/)
Theorem	0in 3969	The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( (/) i^i A ) = (/)
Theorem	inv1 3970	The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.)
|- ( A i^i _V ) = A
Theorem	unv 3971	The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.)
|- ( A u. _V ) = _V
Theorem	0ss 3972	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)
|- (/) C_ A
Theorem	ss0b 3973	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.)
|- ( A C_ (/) <-> A = (/) )
Theorem	ss0 3974	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)
|- ( A C_ (/) -> A = (/) )
Theorem	sseq0 3975	A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A C_ B /\ B = (/) ) -> A = (/) )
Theorem	ssn0 3976	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
|- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )
Theorem	0dif 3977	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
|- ( (/) \ A ) = (/)
Theorem	abf 3978	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
|- -. ph   =>    |- { x | ph } = (/)
Theorem	eq0rdv 3979*	Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
|- ( ph -> -. x e. A )   =>    |- ( ph -> A = (/) )
Theorem	csbprc 3980	The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.) (Proof shortened by JJ, 27-Aug-2021.)
|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
Theorem	csbprcOLD 3981	Obsolete proof of csbprc 3980 as of 27-Aug-2021. (Contributed by NM, 17-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
Theorem	csb0 3982	The proper substitution of a class into the empty set is empty. (Contributed by NM, 18-Aug-2018.)
|- [_ A / x ]_ (/) = (/)
Theorem	sbcel12 3983	Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.)
|- ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. [_ A / x ]_ C )
Theorem	sbceqg 3984	Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
Theorem	sbcnel12g 3985	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
|- ( A e. V -> ( [. A / x ]. B e/ C <-> [_ A / x ]_ B e/ [_ A / x ]_ C ) )
Theorem	sbcne12 3986	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.) (Revised by NM, 18-Aug-2018.)
|- ( [. A / x ]. B =/= C <-> [_ A / x ]_ B =/= [_ A / x ]_ C )
Theorem	sbcel1g 3987*	Move proper substitution in and out of a membership relation. Note that the scope of [. A / x ]. is the wff B e. C, whereas the scope of [_ A / x ]_ is the class B. (Contributed by NM, 10-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. B e. C <-> [_ A / x ]_ B e. C ) )
Theorem	sbceq1g 3988*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = C ) )
Theorem	sbcel2 3989*	Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.)
|- ( [. A / x ]. B e. C <-> B e. [_ A / x ]_ C )
Theorem	sbceq2g 3990*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
|- ( A e. V -> ( [. A / x ]. B = C <-> B = [_ A / x ]_ C ) )
Theorem	csbeq2d 3991	Formula-building deduction rule for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F/ x ph   &    |- ( ph -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )
Theorem	csbeq2dv 3992*	Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- ( ph -> B = C )   =>    |- ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )
Theorem	csbeq2i 3993	Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- B = C   =>    |- [_ A / x ]_ B = [_ A / x ]_ C
Theorem	csbcom 3994*	Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.)
|- [_ A / x ]_ [_ B / y ]_ C = [_ B / y ]_ [_ A / x ]_ C
Theorem	sbcnestgf 3995	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
|- ( ( A e. V /\ A. y F/ x ph ) -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
Theorem	csbnestgf 3996	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|- ( ( A e. V /\ A. y F/_ x C ) -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C )
Theorem	sbcnestg 3997*	Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
Theorem	csbnestg 3998*	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|- ( A e. V -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C )
Theorem	sbcco3g 3999*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|- ( x = A -> B = C )   =>    |- ( A e. V -> ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ph ) )
Theorem	csbco3g 4000*	Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|- ( x = A -> B = C )   =>    |- ( A e. V -> [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ D )