P. 33 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3201-3300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	difin 3201	Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	ddifss 3202	Double complement under universal class. In classical logic (or given an additional hypothesis, as in ddifnel 3103), this is equality rather than subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
⊢ 𝐴 ⊆ (V ∖ (V ∖ 𝐴))
Theorem	unssin 3203	Union as a subset of class complement and intersection (De Morgan's law). One direction of the definition of union in [Mendelson] p. 231. This would be an equality, rather than subset, in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
⊢ (𝐴 ∪ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∩ (V ∖ 𝐵)))
Theorem	inssun 3204	Intersection in terms of class difference and union (De Morgan's law). Similar to Exercise 4.10(n) of [Mendelson] p. 231. This would be an equality, rather than subset, in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
⊢ (𝐴 ∩ 𝐵) ⊆ (V ∖ ((V ∖ 𝐴) ∪ (V ∖ 𝐵)))
Theorem	inssddif 3205	Intersection of two classes and class difference. In classical logic, such as Exercise 4.10(q) of [Mendelson] p. 231, this is an equality rather than subset. (Contributed by Jim Kingdon, 26-Jul-2018.)
⊢ (𝐴 ∩ 𝐵) ⊆ (𝐴 ∖ (𝐴 ∖ 𝐵))
Theorem	invdif 3206	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif 3207	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵)
Theorem	indif2 3208	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indif1 3209	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶)
Theorem	indifcom 3210	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶))
Theorem	indi 3211	Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶))
Theorem	undi 3212	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 3213	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶))
Theorem	undir 3214	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶))
Theorem	uneqin 3215	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 3216	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶))
Theorem	difundir 3217	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
Theorem	difindiss 3218	Distributive law for class difference. In classical logic, for example, theorem 40 of [Suppes] p. 29, this is an equality instead of subset. (Contributed by Jim Kingdon, 26-Jul-2018.)
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∩ 𝐶))
Theorem	difindir 3219	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶))
Theorem	indifdir 3220	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.)
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶))
Theorem	difdif2ss 3221	Set difference with a set difference. In classical logic this would be equality rather than subset. (Contributed by Jim Kingdon, 27-Jul-2018.)
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∖ (𝐵 ∖ 𝐶))
Theorem	undm 3222	De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵))
Theorem	indmss 3223	De Morgan's law for intersection. In classical logic, this would be equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19. (Contributed by Jim Kingdon, 27-Jul-2018.)
⊢ ((V ∖ 𝐴) ∪ (V ∖ 𝐵)) ⊆ (V ∖ (𝐴 ∩ 𝐵))
Theorem	difun1 3224	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶)
Theorem	undif3ss 3225	A subset relationship involving class union and class difference. In classical logic, this would be equality rather than subset, as in the first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Jim Kingdon, 28-Jul-2018.)
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) ⊆ ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴))
Theorem	difin2 3226	Represent a set difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴))
Theorem	dif32 3227	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵)
Theorem	difabs 3228	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵)
Theorem	symdif1 3229	Two ways to express symmetric difference. This theorem shows the equivalence of the definition of symmetric difference in [Stoll] p. 13 and the restated definition in Example 4.1 of [Stoll] p. 262. (Contributed by NM, 17-Aug-2004.)
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = ((𝐴 ∪ 𝐵) ∖ (𝐴 ∩ 𝐵))
2.1.13.5  Class abstractions with difference, union, and intersection of two classes
Theorem	symdifxor 3230*	Expressing symmetric difference with exclusive-or or two differences. (Contributed by Jim Kingdon, 28-Jul-2018.)
⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐴)) = {𝑥 ∣ (𝑥 ∈ 𝐴 ⊻ 𝑥 ∈ 𝐵)}
Theorem	unab 3231	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)}
Theorem	inab 3232	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)}
Theorem	difab 3233	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	notab 3234	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑})
Theorem	unrab 3235	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)}
Theorem	inrab 3236	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	inrab2 3237*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑}
Theorem	difrab 3238	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)}
Theorem	dfrab2 3239*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴)
Theorem	dfrab3 3240*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑})
Theorem	notrab 3241*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
Theorem	dfrab3ss 3242*	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 3243	Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.)
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑})
2.1.13.6  Restricted uniqueness with difference, union, and intersection
Theorem	reuss2 3244*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuss 3245*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun1 3246*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑)
Theorem	reuun2 3247*	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	reupick 3248*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	reupick3 3249*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓))
Theorem	reupick2 3250*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓))
2.1.14  The empty set
Syntax	c0 3251	Extend class notation to include the empty set.
class ∅
Definition	df-nul 3252	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 3253. (Contributed by NM, 5-Aug-1993.)
⊢ ∅ = (V ∖ V)
Theorem	dfnul2 3253	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.)
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
Theorem	dfnul3 3254	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.)
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	noel 3255	The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
⊢ ¬ 𝐴 ∈ ∅
Theorem	n0i 3256	If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2615. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
Theorem	ne0i 3257	If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2615. (Contributed by NM, 31-Dec-1993.)
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
Theorem	vn0 3258	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.)
⊢ V ≠ ∅
Theorem	vn0m 3259	The universal class is inhabited. (Contributed by Jim Kingdon, 17-Dec-2018.)
⊢ ∃𝑥 𝑥 ∈ V
Theorem	n0rf 3260	An inhabited class is nonempty. Following the Definition of [Bauer], p. 483, we call a class 𝐴 nonempty if 𝐴 ≠ ∅ and inhabited if it has at least one element. In classical logic these two concepts are equivalent, for example see Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0r 3261 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by Jim Kingdon, 31-Jul-2018.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅)
Theorem	n0r 3261*	An inhabited class is nonempty. See n0rf 3260 for more discussion. (Contributed by Jim Kingdon, 31-Jul-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅)
Theorem	neq0r 3262*	An inhabited class is nonempty. See n0rf 3260 for more discussion. (Contributed by Jim Kingdon, 31-Jul-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ¬ 𝐴 = ∅)
Theorem	reximdva0m 3263*	Restricted existence deduced from inhabited class. (Contributed by Jim Kingdon, 31-Jul-2018.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)    ⇒   ⊢ ((𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	n0mmoeu 3264*	A case of equivalence of "at most one" and "only one". If a class is inhabited, that class having at most one element is equivalent to it having only one element. (Contributed by Jim Kingdon, 31-Jul-2018.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴))
Theorem	rex0 3265	Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.)
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑
Theorem	eq0 3266*	The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.)
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
Theorem	eqv 3267*	The universe contains every set. (Contributed by NM, 11-Sep-2006.)
⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴)
Theorem	0el 3268*	Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥)
Theorem	abvor0dc 3269*	The class builder of a decidable proposition not containing the abstraction variable is either the universal class or the empty set. (Contributed by Jim Kingdon, 1-Aug-2018.)
⊢ (DECID 𝜑 → ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅))
Theorem	abn0r 3270	Nonempty class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
⊢ (∃𝑥𝜑 → {𝑥 ∣ 𝜑} ≠ ∅)
Theorem	rabn0r 3271	Non-empty restricted class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅)
Theorem	rabn0m 3272*	Inhabited restricted class abstraction. (Contributed by Jim Kingdon, 18-Sep-2018.)
⊢ (∃𝑦 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐴 𝜑)
Theorem	rab0 3273	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.)
⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅
Theorem	rabeq0 3274	Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
Theorem	abeq0 3275	Condition for a class abstraction to be empty. (Contributed by Jim Kingdon, 12-Aug-2018.)
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑)
Theorem	rabxmdc 3276*	Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.)
⊢ (∀𝑥DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}))
Theorem	rabnc 3277*	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅
Theorem	un0 3278	The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∪ ∅) = 𝐴
Theorem	in0 3279	The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
⊢ (𝐴 ∩ ∅) = ∅
Theorem	inv1 3280	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 3281	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 3282	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ ∅ ⊆ 𝐴
Theorem	ss0b 3283	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 3284	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
Theorem	sseq0 3285	A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
Theorem	ssn0 3286	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅)
Theorem	abf 3287	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	eq0rdv 3288*	Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	csbprc 3289	The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
Theorem	un00 3290	Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.)
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅)
Theorem	vss 3291	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	disj 3292*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	disjr 3293*	Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴)
Theorem	disj1 3294*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
Theorem	reldisj 3295	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.)
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))
Theorem	disj3 3296	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵))
Theorem	disjne 3297	Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷)
Theorem	disjel 3298	A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵)
Theorem	disj2 3299	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵))
Theorem	ssdisj 3300	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅)