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	difin2 4301	Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴))
Theorem	dif32 4302	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵)
Theorem	difabs 4303	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	sscon34b 4304	Relative complementation reverses inclusion of subclasses. Relativized version of complss 4151. (Contributed by RP, 3-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)))
Theorem	rcompleq 4305	Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq 4152. (Contributed by RP, 10-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 = 𝐵 ↔ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)))
Theorem	dfsymdif3 4306	Alternate definition of the symmetric difference, given in Example 4.1 of [Stoll] p. 262 (the original definition corresponds to [Stoll] p. 13). (Contributed by NM, 17-Aug-2004.) (Revised by BJ, 30-Apr-2020.)
⊢ (𝐴 △ 𝐵) = ((𝐴 ∪ 𝐵) ∖ (𝐴 ∩ 𝐵))
2.1.13.6  Class abstractions with difference, union, and intersection of two classes
Theorem	unabw 4307*	Union of two class abstractions. Version of unab 4308 using implicit substitution, which does not require ax-8 2110, ax-10 2141, ax-12 2177. (Contributed by GG, 15-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    ⇒   ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑦 ∣ (𝜒 ∨ 𝜃)}
Theorem	unab 4308	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}
Theorem	inab 4309	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)}
Theorem	difab 4310	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	abanssl 4311	A class abstraction with a conjunction is a subset of the class abstraction with the left conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.)
⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜑}
Theorem	abanssr 4312	A class abstraction with a conjunction is a subset of the class abstraction with the right conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.)
⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜓}
Theorem	notabw 4313*	A class abstraction defined by a negation. Version of notab 4314 using implicit substitution, which does not require ax-10 2141, ax-12 2177. (Contributed by GG, 15-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑦 ∣ 𝜓})
Theorem	notab 4314	A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010.)
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑})
Theorem	unrab 4315	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}
Theorem	inrab 4316	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	inrab2 4317*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑}
Theorem	difrab 4318	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	dfrab3 4319*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑})
Theorem	dfrab2 4320*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴)
Theorem	rabdif 4321*	Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ 𝐵) = {𝑥 ∈ (𝐴 ∖ 𝐵) ∣ 𝜑}
Theorem	notrab 4322*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
Theorem	dfrab3ss 4323*	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 4324	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	reuun2 4325	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Wolf Lammen, 15-May-2025.)
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	reuss2 4326*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuss 4327*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun1 4328*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reupick 4329*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	reupick3 4330*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
Theorem	reupick2 4331*	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 4332*	Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴)
2.1.14  The empty set
Syntax	c0 4333	Extend class notation to include the empty set.
class ∅
Definition	df-nul 4334	Define the empty set. More precisely, we should write "empty class". It will be posited in ax-nul 5306 that an empty set exists. Then, by uniqueness among classes (eq0 4350, as opposed to the weaker uniqueness among sets, nulmo 2713), it will follow that ∅ is indeed a set (0ex 5307). Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 4336. (Contributed by NM, 17-Jun-1993.) Clarify that at this point, it is not established that it is a set. (Revised by BJ, 22-Sep-2022.)
⊢ ∅ = (V ∖ V)
Theorem	dfnul4 4335	Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) Avoid ax-8 2110, df-clel 2816. (Revised by GG, 3-Sep-2024.) Prove directly from definition to allow shortening dfnul2 4336. (Revised by BJ, 23-Sep-2024.)
⊢ ∅ = {𝑥 ∣ ⊥}
Theorem	dfnul2 4336	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Remove dependency on ax-10 2141, ax-11 2157, and ax-12 2177. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
Theorem	dfnul3 4337	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	noel 4338	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.) Remove dependency on ax-10 2141, ax-11 2157, and ax-12 2177. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)
⊢ ¬ 𝐴 ∈ ∅
Theorem	nel02 4339	The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.)
⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
Theorem	n0i 4340	If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
Theorem	ne0i 4341	If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
Theorem	ne0d 4342	Deduction form of ne0i 4341. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	n0ii 4343	If a class has elements, then it is not empty. Inference associated with n0i 4340. (Contributed by BJ, 15-Jul-2021.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ¬ 𝐵 = ∅
Theorem	ne0ii 4344	If a class has elements, then it is nonempty. Inference associated with ne0i 4341. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐵 ≠ ∅
Theorem	vn0 4345	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.) Avoid ax-8 2110, df-clel 2816. (Revised by GG, 6-Sep-2024.)
⊢ V ≠ ∅
Theorem	vn0ALT 4346	Alternate proof of vn0 4345. Shorter, but requiring df-clel 2816, ax-8 2110. (Contributed by NM, 11-Sep-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ V ≠ ∅
Theorem	eq0f 4347	A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by BJ, 15-Jul-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
Theorem	neq0f 4348	A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of neq0 4352 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by BJ, 15-Jul-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	n0f 4349	A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 4353 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by NM, 17-Oct-2003.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	eq0 4350*	A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2157, ax-12 2177. (Revised by GG and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2110, df-clel 2816. (Revised by GG, 6-Sep-2024.)
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
Theorem	eq0ALT 4351*	Alternate proof of eq0 4350. Shorter, but requiring df-clel 2816, ax-8 2110. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2157, ax-12 2177. (Revised by GG and Steven Nguyen, 28-Jun-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
Theorem	neq0 4352*	A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) Avoid ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.)
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	n0 4353*	A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.) Avoid ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.)
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	nel0 4354*	From the general negation of membership in 𝐴, infer that 𝐴 is the empty set. (Contributed by BJ, 6-Oct-2018.)
⊢ ¬ 𝑥 ∈ 𝐴    ⇒   ⊢ 𝐴 = ∅
Theorem	reximdva0 4355*	Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	rspn0 4356*	Specialization for restricted generalization with a nonempty class. (Contributed by Alexander van der Vekens, 6-Sep-2018.) Avoid ax-10 2141, ax-12 2177. (Revised by GG, 28-Jun-2024.)
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑))
Theorem	n0rex 4357*	There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐴)
Theorem	ssn0rex 4358*	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 4359*	A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.)
⊢ (𝐴 ≠ ∅ → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴))
Theorem	rex0 4360	Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.)
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑
Theorem	reu0 4361	Vacuous restricted uniqueness is always false. (Contributed by AV, 3-Apr-2023.)
⊢ ¬ ∃!𝑥 ∈ ∅ 𝜑
Theorem	rmo0 4362	Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023.)
⊢ ∃*𝑥 ∈ ∅ 𝜑
Theorem	0el 4363*	Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	n0el 4364*	Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (¬ ∅ ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑢 𝑢 ∈ 𝑥)
Theorem	eqeuel 4365*	A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) → ∃!𝑥 𝑥 ∈ 𝐴)
Theorem	ssdif0 4366	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)
Theorem	difn0 4367	If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017.)
⊢ ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐴 ≠ 𝐵)
Theorem	pssdifn0 4368	A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	pssdif 4369	A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	ndisj 4370*	Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.)
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	inn0f 4371	A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	inn0 4372*	A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	difin0ss 4373	Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
⊢ (((𝐴 ∖ 𝐵) ∩ 𝐶) = ∅ → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
Theorem	inssdif0 4374	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	inindif 4375	The intersection and class difference of a class with another class are disjoint. With inundif 4479, this shows that such intersection and class difference partition the class 𝐴. (Contributed by Thierry Arnoux, 13-Sep-2017.)
⊢ ((𝐴 ∩ 𝐶) ∩ (𝐴 ∖ 𝐶)) = ∅
Theorem	difid 4376	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 4377	Alternate proof of difid 4376. Shorter, but requiring ax-8 2110, df-clel 2816. (Contributed by NM, 22-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∖ 𝐴) = ∅
Theorem	dif0 4378	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 4379*	The class of sets verifying a property is the empty class if and only if that property is a contradiction. Version of ab0 4380 using implicit substitution, which requires fewer axioms. (Contributed by GG, 3-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑦 ¬ 𝜓)
Theorem	ab0 4380	The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 4385 (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 2941). (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2816, ax-8 2110. (Revised by GG, 30-Aug-2024.) (Proof shortened by SN, 8-Sep-2024.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	ab0ALT 4381	Alternate proof of ab0 4380, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	dfnf5 4382	Characterization of nonfreeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥𝜑 ↔ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅))
Theorem	ab0orv 4383*	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 GG, 30-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)
Theorem	ab0orvALT 4384*	Alternate proof of ab0orv 4383, 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 4385	Nonempty class abstraction. See also ab0 4380. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2816, ax-8 2110. (Revised by GG, 30-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Theorem	rab0 4386	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 4387*	Condition for a restricted class abstraction to be empty. Version of rabeq0 4388 using implicit substitution, which does not require ax-10 2141, ax-11 2157, ax-12 2177, but requires ax-8 2110. (Contributed by GG, 30-Sep-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
Theorem	rabeq0 4388	Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rabn0 4389	Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rabxm 4390*	Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})
Theorem	rabnc 4391	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅
Theorem	elneldisj 4392*	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 4393*	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 4394	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 4395	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 4396	The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (∅ ∪ 𝐴) = 𝐴
Theorem	0in 4397	The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (∅ ∩ 𝐴) = ∅
Theorem	inv1 4398	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 4399	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 4400	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)
⊢ ∅ ⊆ 𝐴