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.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	dfrab3 3902*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑})
Theorem	dfrab2 3903*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴)
Theorem	notrab 3904*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
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.)
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}))
Theorem	rabun2 3906	Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.)
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑})
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.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuss 3908*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun1 3909*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun2 3910*	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	reupick 3911*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	reupick3 3912*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
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.)
⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓))
Theorem	euelss 3914*	Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴)
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.)
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
Theorem	dfnul3 3918	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.)
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
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.)
⊢ ¬ 𝐴 ∈ ∅
Theorem	n0i 3920	If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
Theorem	ne0i 3921	If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
Theorem	n0ii 3922	If a set has elements, then it is not empty. Inference associated with n0i 3920. (Contributed by BJ, 15-Jul-2021.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ¬ 𝐵 = ∅
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.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐵 ≠ ∅
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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
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 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by BJ, 15-Jul-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
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 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by NM, 17-Oct-2003.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
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.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	eq0 3929*	The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.)
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
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.)
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
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.)
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	nel0 3932*	From the general negation of membership in 𝐴, infer that 𝐴 is the empty set. (Contributed by BJ, 6-Oct-2018.)
⊢ ¬ 𝑥 ∈ 𝐴    ⇒   ⊢ 𝐴 = ∅
Theorem	reximdva0 3933*	Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	rspn0 3934*	Specialization for restricted generalization with a nonempty set. (Contributed by Alexander van der Vekens, 6-Sep-2018.)
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑))
Theorem	n0rex 3935*	There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐴)
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.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐵 𝑥 ∈ 𝐴)
Theorem	n0moeu 3937*	A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.)
⊢ (𝐴 ≠ ∅ → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴))
Theorem	rex0 3938	Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.)
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑
Theorem	0el 3939*	Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	n0el 3940*	Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (¬ ∅ ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑢 𝑢 ∈ 𝑥)
Theorem	eqeuel 3941*	A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) → ∃!𝑥 𝑥 ∈ 𝐴)
Theorem	ssdif0 3942	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)
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.)
⊢ ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐴 ≠ 𝐵)
Theorem	pssdifn0 3944	A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	pssdif 3945	A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	difin0ss 3946	Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
⊢ (((𝐴 ∖ 𝐵) ∩ 𝐶) = ∅ → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
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.)
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ∅)
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.)
⊢ (𝐴 ∖ 𝐴) = ∅
Theorem	difidALT 3949	Alternate proof of difid 3948. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∖ 𝐴) = ∅
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.)
⊢ (𝐴 ∖ ∅) = 𝐴
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.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	dfnf5 3952	Characterization of non-freeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥𝜑 ↔ ({𝑥 ∣ 𝜑} = ∅ ∨ {𝑥 ∣ 𝜑} = 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.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ∨ {𝑥 ∣ 𝜑} = 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.)
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
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.)
⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅
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.)
⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅
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.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rabn0 3958	Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)
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.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)
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.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rabxm 3961*	Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})
Theorem	rabnc 3962*	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅
Theorem	elneldisj 3963*	The set of elements 𝑠 determining classes 𝐶 (which may depend on 𝑠) containing a special element and the set of elements 𝑠 determining classes 𝐶 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.)
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}    &   ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶}    ⇒   ⊢ (𝐸 ∩ 𝑁) = ∅
Theorem	elnelun 3964*	The union of the set of elements 𝑠 determining classes 𝐶 (which may depend on 𝑠) containing a special element and the set of elements 𝑠 determining classes 𝐶 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.)
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}    &   ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶}    ⇒   ⊢ (𝐸 ∪ 𝑁) = 𝐴
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.)
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝑠}    &   ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝑠}    ⇒   ⊢ (𝐸 ∩ 𝑁) = ∅
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.)
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝑠}    &   ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝑠}    ⇒   ⊢ (𝐸 ∪ 𝑁) = 𝐴
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.)
⊢ (𝐴 ∪ ∅) = 𝐴
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.)
⊢ (𝐴 ∩ ∅) = ∅
Theorem	0in 3969	The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (∅ ∩ 𝐴) = ∅
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.)
⊢ (𝐴 ∩ V) = 𝐴
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.)
⊢ (𝐴 ∪ 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.)
⊢ ∅ ⊆ 𝐴
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.)
⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
Theorem	ss0 3974	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
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.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
Theorem	ssn0 3976	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)
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.)
⊢ (∅ ∖ 𝐴) = ∅
Theorem	abf 3978	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	eq0rdv 3979*	Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
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.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
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.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
Theorem	csb0 3982	The proper substitution of a class into the empty set is empty. (Contributed by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌∅ = ∅
Theorem	sbcel12 3983	Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbceqg 3984	Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcnel12g 3985	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∉ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∉ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcne12 3986	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbcel1g 3987*	Move proper substitution in and out of a membership relation. Note that the scope of [𝐴 / 𝑥] is the wff 𝐵 ∈ 𝐶, whereas the scope of ⦋𝐴 / 𝑥⦌ is the class 𝐵. (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝐶))
Theorem	sbceq1g 3988*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
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.)
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbceq2g 3990*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbeq2d 3991	Formula-building deduction rule for class substitution. (Contributed by NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2dv 3992*	Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbeq2i 3993	Formula-building inference rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶
Theorem	csbcom 3994*	Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶
Theorem	sbcnestgf 3995	Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestgf 3996	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcnestg 3997*	Nest the composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestg 3998*	Nest the composition of two substitutions. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcco3g 3999*	Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑))
Theorem	csbco3g 4000*	Composition of two class substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷)