P. 43 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	undi 4201	Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∪ (𝐵 ∩ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ 𝐶))
Theorem	indir 4202	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))
Theorem	undir 4203	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶))
Theorem	unineq 4204	Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse. (Contributed by NM, 10-Aug-2004.)
⊢ (((𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) ↔ 𝐴 = 𝐵)
Theorem	uneqin 4205	Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵)
Theorem	difundi 4206	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶))
Theorem	difundir 4207	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
Theorem	difindi 4208	Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶))
Theorem	difindir 4209	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶))
Theorem	indifdir 4210	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.)
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶))
Theorem	difdif2 4211	Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.)
⊢ (𝐴 ∖ (𝐵 ∖ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶))
Theorem	undm 4212	De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵))
Theorem	indm 4213	De Morgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
⊢ (V ∖ (𝐴 ∩ 𝐵)) = ((V ∖ 𝐴) ∪ (V ∖ 𝐵))
Theorem	difun1 4214	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶)
Theorem	undif3 4215	An equality involving class union and class difference. The first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 17-Apr-2012.) (Proof shortened by JJ, 13-Jul-2021.)
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))
Theorem	difin2 4216	Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴))
Theorem	dif32 4217	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵)
Theorem	difabs 4218	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	sscon34b 4219	Relative complementation reverses inclusion of subclasses. Relativized version of complss 4074. (Contributed by RP, 3-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)))
Theorem	rcompleq 4220	Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq 4075. (Contributed by RP, 10-Jun-2021.)
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 = 𝐵 ↔ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)))
Theorem	dfsymdif3 4221	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	unab 4222	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}
Theorem	inab 4223	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)}
Theorem	difab 4224	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	notab 4225	A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010.)
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑})
Theorem	unrab 4226	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}
Theorem	inrab 4227	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	inrab2 4228*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑}
Theorem	difrab 4229	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	dfrab3 4230*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑})
Theorem	dfrab2 4231*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴)
Theorem	notrab 4232*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
Theorem	dfrab3ss 4233*	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 4234	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 4235*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuss 4236*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun1 4237*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun2 4238*	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	reupick 4239*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	reupick3 4240*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
Theorem	reupick2 4241*	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 4242*	Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴)
2.1.14  The empty set
Syntax	c0 4243	Extend class notation to include the empty set.
class ∅
Definition	df-nul 4244	Define the empty set. More precisely, we should write "empty class". It will be posited in ax-nul 5174 that an empty set exists. Then, by uniqueness among classes (eq0 4258, as opposed to the weaker uniqueness among sets, nulmo 2775), it will follow that ∅ is indeed a set (0ex 5175). Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 4245. (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	dfnul2 4245	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Remove dependency on ax-10 2142, ax-11 2158, and ax-12 2175. (Revised by Steven Nguyen, 3-May-2023.)
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
Theorem	dfnul3 4246	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.)
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	noel 4247	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 2142, ax-11 2158, and ax-12 2175. (Revised by Steven Nguyen, 3-May-2023.)
⊢ ¬ 𝐴 ∈ ∅
Theorem	nel02 4248	The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.)
⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴)
Theorem	n0i 4249	If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
Theorem	ne0i 4250	If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
Theorem	ne0d 4251	Deduction form of ne0i 4250. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	n0ii 4252	If a class has elements, then it is not empty. Inference associated with n0i 4249. (Contributed by BJ, 15-Jul-2021.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ¬ 𝐵 = ∅
Theorem	ne0ii 4253	If a class has elements, then it is nonempty. Inference associated with ne0i 4250. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐵 ≠ ∅
Theorem	vn0 4254	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.)
⊢ V ≠ ∅
Theorem	eq0f 4255	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 4256	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 4259 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by BJ, 15-Jul-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	n0f 4257	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 4260 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by NM, 17-Oct-2003.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	eq0 4258*	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 2158, ax-12 2175. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.)
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
Theorem	neq0 4259*	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 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	n0 4260*	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 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	eq0OLD 4261*	Obsolete version of eq0 4258 as of 28-Jun-2024. (Contributed by NM, 29-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
Theorem	neq0OLD 4262*	Obsolete version of neq0 4259 as of 28-Jun-2024. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	n0OLD 4263*	Obsolete version of n0 4260 as of 28-Jun-2024. (Contributed by NM, 29-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
Theorem	nel0 4264*	From the general negation of membership in 𝐴, infer that 𝐴 is the empty set. (Contributed by BJ, 6-Oct-2018.)
⊢ ¬ 𝑥 ∈ 𝐴    ⇒   ⊢ 𝐴 = ∅
Theorem	reximdva0 4265*	Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	rspn0 4266*	Specialization for restricted generalization with a nonempty class. (Contributed by Alexander van der Vekens, 6-Sep-2018.) Avoid ax-10 2142, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑))
Theorem	rspn0OLD 4267*	Obsolete version of rspn0 4266 as of 28-Jun-2024. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑))
Theorem	n0rex 4268*	There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐴)
Theorem	ssn0rex 4269*	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 4270*	A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.)
⊢ (𝐴 ≠ ∅ → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴))
Theorem	rex0 4271	Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.)
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑
Theorem	reu0 4272	Vacuous restricted uniqueness is always false. (Contributed by AV, 3-Apr-2023.)
⊢ ¬ ∃!𝑥 ∈ ∅ 𝜑
Theorem	rmo0 4273	Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023.)
⊢ ∃*𝑥 ∈ ∅ 𝜑
Theorem	0el 4274*	Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	n0el 4275*	Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (¬ ∅ ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑢 𝑢 ∈ 𝑥)
Theorem	eqeuel 4276*	A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) → ∃!𝑥 𝑥 ∈ 𝐴)
Theorem	ssdif0 4277	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)
Theorem	difn0 4278	If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017.)
⊢ ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐴 ≠ 𝐵)
Theorem	pssdifn0 4279	A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	pssdif 4280	A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	ndisj 4281*	Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.)
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	difin0ss 4282	Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
⊢ (((𝐴 ∖ 𝐵) ∩ 𝐶) = ∅ → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
Theorem	inssdif0 4283	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 4284	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 4285	Alternate proof of difid 4284. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∖ 𝐴) = ∅
Theorem	dif0 4286	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 4287	The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 4290 (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 2988). (Contributed by BJ, 19-Mar-2021.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	dfnf5 4288	Characterization of non-freeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥𝜑 ↔ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅))
Theorem	ab0orv 4289*	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.)
⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)
Theorem	abn0 4290	Nonempty class abstraction. See also ab0 4287. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑)
Theorem	rab0 4291	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	rabeq0 4292	Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	rabn0 4293	Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rabxm 4294*	Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑})
Theorem	rabnc 4295*	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅
Theorem	elneldisj 4296*	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 4297*	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 4298	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 4299	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 4300	The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (∅ ∪ 𝐴) = 𝐴