P. 44 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4301-4400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	difid 4301	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.) (Revised by David Abernethy, 17-Jun-2012.)
⊢ (𝐴 ∖ 𝐴) = ∅
Theorem	difidALT 4302	Alternate proof of difid 4301. Shorter, but requiring ax-8 2110, df-clel 2817. (Contributed by NM, 22-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∖ 𝐴) = ∅
Theorem	dif0 4303	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	ab0w 4304*	The class of sets verifying a property is the empty class if and only if that property is a contradiction. Version of ab0 4305 using implicit substitution, which requires fewer axioms. (Contributed by Gino Giotto, 3-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑦 ¬ 𝜓)
Theorem	ab0 4305	The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 4311 (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 2943). (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2817, ax-8 2110. (Revised by Gino Giotto, 30-Aug-2024.) (Proof shortened by SN, 8-Sep-2024.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	ab0OLD 4306	Obsolete version of ab0 4305 as of 8-Sep-2024. (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2817, ax-8 2110. (Revised by Gino Giotto, 30-Aug-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	ab0ALT 4307	Alternate proof of ab0 4305, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	dfnf5 4308	Characterization of nonfreeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥𝜑 ↔ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅))
Theorem	ab0orv 4309*	The class abstraction defined by a formula 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.) Reduce axiom usage. (Revised by Gino Giotto, 30-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)
Theorem	ab0orvALT 4310*	Alternate proof of ab0orv 4309, shorter but using more axioms. (Contributed by Mario Carneiro, 29-Aug-2013.) (Revised by BJ, 22-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)
Theorem	abn0 4311	Nonempty class abstraction. See also ab0 4305. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2817, ax-8 2110. (Revised by Gino Giotto, 30-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Theorem	abn0OLD 4312	Obsolete version of abn0 4311 as of 30-Aug-2024. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Theorem	rab0 4313	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	rabeq0w 4314*	Condition for a restricted class abstraction to be empty. Version of rabeq0 4315 using implicit substitution, which does not require ax-10 2139, ax-11 2156, ax-12 2173, but requires ax-8 2110. (Contributed by Gino Giotto, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
Theorem	rabeq0 4315	Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rabn0 4316	Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rabxm 4317*	Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})
Theorem	rabnc 4318	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅
Theorem	elneldisj 4319*	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 4320*	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	un0 4321	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 4322	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	0un 4323	The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (∅ ∪ 𝐴) = 𝐴
Theorem	0in 4324	The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (∅ ∩ 𝐴) = ∅
Theorem	inv1 4325	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 4326	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 4327	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 4328	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 4329	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
Theorem	sseq0 4330	A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
Theorem	ssn0 4331	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)
Theorem	0dif 4332	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 4333	A class abstraction determined by a false formula is empty. (Contributed by NM, 20-Jan-2012.) Avoid ax-8 2110, ax-10 2139, ax-11 2156, ax-12 2173. (Revised by Gino Giotto, 30-Jun-2024.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	abfOLD 4334	Obsolete version of abf 4333 as of 28-Jun-2024. (Contributed by NM, 20-Jan-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	eq0rdv 4335*	Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2110, df-clel 2817. (Revised by Gino Giotto, 6-Sep-2024.)
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	eq0rdvALT 4336*	Alternate proof of eq0rdv 4335. Shorter, but requiring df-clel 2817, ax-8 2110. (Contributed by NM, 11-Jul-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	csbprc 4337	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	csb0 4338	The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌∅ = ∅
Theorem	sbcel12 4339	Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbceqg 4340	Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbceqi 4341	Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷    &   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = 𝐸    ⇒   ⊢ ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐷 = 𝐸)
Theorem	sbcnel12g 4342	Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∉ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∉ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	sbcne12 4343	Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbcel1g 4344*	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 4345*	Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶))
Theorem	sbcel2 4346*	Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	sbceq2g 4347*	Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbcom 4348*	Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶
Theorem	sbcnestgfw 4349*	Nest the composition of two substitutions. Version of sbcnestgf 4354 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 11-Nov-2016.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestgfw 4350*	Nest the composition of two substitutions. Version of csbnestgf 4355 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 23-Nov-2005.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcnestgw 4351*	Nest the composition of two substitutions. Version of sbcnestg 4356 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 27-Nov-2005.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestgw 4352*	Nest the composition of two substitutions. Version of csbnestg 4357 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 23-Nov-2005.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcco3gw 4353*	Composition of two substitutions. Version of sbcco3g 4358 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 27-Nov-2005.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑))
Theorem	sbcnestgf 4354	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcnestgfw 4349 when possible. (Contributed by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestgf 4355	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker csbnestgfw 4350 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcnestg 4356*	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcnestgw 4351 when possible. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))
Theorem	csbnestg 4357*	Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker csbnestgw 4352 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶)
Theorem	sbcco3g 4358*	Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcco3gw 4353 when possible. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑))
Theorem	csbco3g 4359*	Composition of two class substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷)
Theorem	csbnest1g 4360	Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶)
Theorem	csbidm 4361*	Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵
Theorem	csbvarg 4362	The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴)
Theorem	csbvargi 4363	The proper substitution of a class for a setvar variable results in the class (if the class exists), in inference form of csbvarg 4362. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝑥 = 𝐴
Theorem	sbccsb 4364*	Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑})
Theorem	sbccsb2 4365	Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.) (Revised by NM, 18-Aug-2018.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ ⦋𝐴 / 𝑥⦌{𝑥 ∣ 𝜑})
Theorem	rspcsbela 4366*	Special case related to rspsbc 3808. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)
Theorem	sbnfc2 4367*	Two ways of expressing "𝑥 is (effectively) not free in 𝐴". (Contributed by Mario Carneiro, 14-Oct-2016.)
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴)
Theorem	csbab 4368*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑}
Theorem	csbun 4369	Distribution of class substitution over union of two classes. (Contributed by Drahflow, 23-Sep-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by NM, 13-Sep-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∪ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∪ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbin 4370	Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) (Revised by NM, 18-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌𝐶)
Theorem	csbie2df 4371*	Conversion of implicit substitution to explicit class substitution. This version of csbiedf 3859 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. Deduction form of csbie2 3870. (Contributed by AV, 29-Mar-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐶)    &   ⊢ (𝜑 → Ⅎ𝑥𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷)
Theorem	2nreu 4372*	If there are two different sets fulfilling a wff (by implicit substitution), then there is no unique set fulfilling the wff. (Contributed by AV, 20-Jun-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑))
Theorem	un00 4373	Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.)
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
Theorem	vss 4374	Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (V ⊆ 𝐴 ↔ 𝐴 = V)
Theorem	0pss 4375	The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.)
⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅)
Theorem	npss0 4376	No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ¬ 𝐴 ⊊ ∅
Theorem	pssv 4377	Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.)
⊢ (𝐴 ⊊ V ↔ ¬ 𝐴 = V)
Theorem	disj 4378*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2139, ax-11 2156, ax-12 2173. (Revised by Gino Giotto, 28-Jun-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	disjOLD 4379*	Obsolete version of disj 4378 as of 28-Jun-2024. (Contributed by NM, 17-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	disjr 4380*	Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴)
Theorem	disj1 4381*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
Theorem	reldisj 4382	Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid ax-12 2173. (Revised by Gino Giotto, 28-Jun-2024.)
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))
Theorem	reldisjOLD 4383	Obsolete version of reldisj 4382 as of 28-Jun-2024. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))
Theorem	disj3 4384	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))
Theorem	disjne 4385	Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷)
Theorem	disjeq0 4386	Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 = 𝐵 ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
Theorem	disjel 4387	A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵)
Theorem	disj2 4388	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵))
Theorem	disj4 4389	Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ¬ (𝐴 ∖ 𝐵) ⊊ 𝐴)
Theorem	ssdisj 4390	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅)
Theorem	disjpss 4391	A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵))
Theorem	undisj1 4392	The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅)
Theorem	undisj2 4393	The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅)
Theorem	ssindif0 4394	Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ (V ∖ 𝐵)) = ∅)
Theorem	inelcm 4395	The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅)
Theorem	minel 4396	A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) (Proof shortened by JJ, 14-Jul-2021.)
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶)
Theorem	undif4 4397	Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶))
Theorem	disjssun 4398	Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶))
Theorem	vdif0 4399	Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅)
Theorem	difrab0eq 4400*	If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
⊢ ((𝑉 ∖ {𝑥 ∈ 𝑉 ∣ 𝜑}) = ∅ ↔ 𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑})