P. 36 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 3501-3600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	indifcom 3501	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ (A ∩ (B ∖ C)) = (B ∩ (A ∖ C))
Theorem	indi 3502	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.)
⊢ (A ∩ (B ∪ C)) = ((A ∩ B) ∪ (A ∩ C))
Theorem	undi 3503	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.)
⊢ (A ∪ (B ∩ C)) = ((A ∪ B) ∩ (A ∪ C))
Theorem	indir 3504	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((A ∪ B) ∩ C) = ((A ∩ C) ∪ (B ∩ C))
Theorem	undir 3505	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
⊢ ((A ∩ B) ∪ C) = ((A ∪ C) ∩ (B ∪ C))
Theorem	unineq 3506	Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse. (Contributed by NM, 10-Aug-2004.)
⊢ (((A ∪ C) = (B ∪ C) ∧ (A ∩ C) = (B ∩ C)) ↔ A = B)
Theorem	uneqin 3507	Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((A ∪ B) = (A ∩ B) ↔ A = B)
Theorem	difundi 3508	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (A ∖ (B ∪ C)) = ((A ∖ B) ∩ (A ∖ C))
Theorem	difundir 3509	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((A ∪ B) ∖ C) = ((A ∖ C) ∪ (B ∖ C))
Theorem	difindi 3510	Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
⊢ (A ∖ (B ∩ C)) = ((A ∖ B) ∪ (A ∖ C))
Theorem	difindir 3511	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
⊢ ((A ∩ B) ∖ C) = ((A ∖ C) ∩ (B ∖ C))
Theorem	indifdir 3512	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.)
⊢ ((A ∖ B) ∩ C) = ((A ∩ C) ∖ (B ∩ C))
Theorem	undm 3513	De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
⊢ (V ∖ (A ∪ B)) = ((V ∖ A) ∩ (V ∖ B))
Theorem	indm 3514	De Morgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
⊢ (V ∖ (A ∩ B)) = ((V ∖ A) ∪ (V ∖ B))
Theorem	difun1 3515	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
⊢ (A ∖ (B ∪ C)) = ((A ∖ B) ∖ C)
Theorem	undif3 3516	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.)
⊢ (A ∪ (B ∖ C)) = ((A ∪ B) ∖ (C ∖ A))
Theorem	difin2 3517	Represent a set difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (A ⊆ C → (A ∖ B) = ((C ∖ B) ∩ A))
Theorem	dif32 3518	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
⊢ ((A ∖ B) ∖ C) = ((A ∖ C) ∖ B)
Theorem	difabs 3519	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
⊢ ((A ∖ B) ∖ B) = (A ∖ B)
Theorem	symdif1 3520	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.)
⊢ ((A ∖ B) ∪ (B ∖ A)) = ((A ∪ B) ∖ (A ∩ B))
Theorem	symdif2 3521*	Two ways to express symmetric difference. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((A ∖ B) ∪ (B ∖ A)) = {x ∣ ¬ (x ∈ A ↔ x ∈ B)}
Theorem	unab 3522	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({x ∣ φ} ∪ {x ∣ ψ}) = {x ∣ (φ ∨ ψ)}
Theorem	inab 3523	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({x ∣ φ} ∩ {x ∣ ψ}) = {x ∣ (φ ∧ ψ)}
Theorem	difab 3524	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ({x ∣ φ} ∖ {x ∣ ψ}) = {x ∣ (φ ∧ ¬ ψ)}
Theorem	complab 3525	Complement of a class abstraction. (Contributed by SF, 12-Jan-2015.)
⊢ ∼ {x ∣ φ} = {x ∣ ¬ φ}
Theorem	notab 3526	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
⊢ {x ∣ ¬ φ} = (V ∖ {x ∣ φ})
Theorem	unrab 3527	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
⊢ ({x ∈ A ∣ φ} ∪ {x ∈ A ∣ ψ}) = {x ∈ A ∣ (φ ∨ ψ)}
Theorem	inrab 3528	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
⊢ ({x ∈ A ∣ φ} ∩ {x ∈ A ∣ ψ}) = {x ∈ A ∣ (φ ∧ ψ)}
Theorem	inrab2 3529*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
⊢ ({x ∈ A ∣ φ} ∩ B) = {x ∈ (A ∩ B) ∣ φ}
Theorem	difrab 3530	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
⊢ ({x ∈ A ∣ φ} ∖ {x ∈ A ∣ ψ}) = {x ∈ A ∣ (φ ∧ ¬ ψ)}
Theorem	dfrab2 3531*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.)
⊢ {x ∈ A ∣ φ} = ({x ∣ φ} ∩ A)
Theorem	dfrab3 3532*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
⊢ {x ∈ A ∣ φ} = (A ∩ {x ∣ φ})
Theorem	notrab 3533*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (A ∖ {x ∈ A ∣ φ}) = {x ∈ A ∣ ¬ φ}
Theorem	dfrab3ss 3534*	Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 8-Nov-2015.)
⊢ (A ⊆ B → {x ∈ A ∣ φ} = (A ∩ {x ∈ B ∣ φ}))
Theorem	rabun2 3535	Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.)
⊢ {x ∈ (A ∪ B) ∣ φ} = ({x ∈ A ∣ φ} ∪ {x ∈ B ∣ φ})
Theorem	reuss2 3536*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
⊢ (((A ⊆ B ∧ ∀x ∈ A (φ → ψ)) ∧ (∃x ∈ A φ ∧ ∃!x ∈ B ψ)) → ∃!x ∈ A φ)
Theorem	reuss 3537*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
⊢ ((A ⊆ B ∧ ∃x ∈ A φ ∧ ∃!x ∈ B φ) → ∃!x ∈ A φ)
Theorem	reuun1 3538*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
⊢ ((∃x ∈ A φ ∧ ∃!x ∈ (A ∪ B)(φ ∨ ψ)) → ∃!x ∈ A φ)
Theorem	reuun2 3539*	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)
⊢ (¬ ∃x ∈ B φ → (∃!x ∈ (A ∪ B)φ ↔ ∃!x ∈ A φ))
Theorem	reupick 3540*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
⊢ (((A ⊆ B ∧ (∃x ∈ A φ ∧ ∃!x ∈ B φ)) ∧ φ) → (x ∈ A ↔ x ∈ B))
Theorem	reupick3 3541*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
⊢ ((∃!x ∈ A φ ∧ ∃x ∈ A (φ ∧ ψ) ∧ x ∈ A) → (φ → ψ))
Theorem	reupick2 3542*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
⊢ (((∀x ∈ A (ψ → φ) ∧ ∃x ∈ A ψ ∧ ∃!x ∈ A φ) ∧ x ∈ A) → (φ ↔ ψ))
Theorem	symdifcom 3543	Symmetric difference commutes. (Contributed by SF, 11-Jan-2015.)
⊢ (A ⊕ B) = (B ⊕ A)
Theorem	compleqb 3544	Two classes are equal iff their complements are equal. (Contributed by SF, 11-Jan-2015.)
⊢ (A = B ↔ ∼ A = ∼ B)
Theorem	necompl 3545	A class is not equal to its complement. (Contributed by SF, 11-Jan-2015.)
⊢ ∼ A ≠ A
Theorem	dfin5 3546	Definition of intersection in terms of union. (Contributed by SF, 12-Jan-2015.)
⊢ (A ∩ B) = ∼ ( ∼ A ∪ ∼ B)
Theorem	dfun4 3547	Definition of union in terms of intersection. (Contributed by SF, 12-Jan-2015.)
⊢ (A ∪ B) = ∼ ( ∼ A ∩ ∼ B)
Theorem	iunin 3548	Intersection of two complements is equal to the complement of a union. (Contributed by SF, 12-Jan-2015.)
⊢ ∼ (A ∪ B) = ( ∼ A ∩ ∼ B)
Theorem	iinun 3549	Complement of intersection is equal to union of complements. (Contributed by SF, 12-Jan-2015.)
⊢ ∼ (A ∩ B) = ( ∼ A ∪ ∼ B)
Theorem	difsscompl 3550	A difference is a subset of the complement of its second argument. (Contributed by SF, 10-Mar-2015.)
⊢ (A ∖ B) ⊆ ∼ B
2.1.13  The empty set
Syntax	c0 3551	Extend class notation to include the empty set.
class ∅
Definition	df-nul 3552	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 3553. (Contributed by NM, 5-Aug-1993.)
⊢ ∅ = (V ∖ V)
Theorem	dfnul2 3553	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.)
⊢ ∅ = {x ∣ ¬ x = x}
Theorem	dfnul3 3554	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.)
⊢ ∅ = {x ∈ A ∣ ¬ x ∈ A}
Theorem	noel 3555	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.)
⊢ ¬ A ∈ ∅
Theorem	n0i 3556	If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)
⊢ (B ∈ A → ¬ A = ∅)
Theorem	ne0i 3557	If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)
⊢ (B ∈ A → A ≠ ∅)
Theorem	vn0 3558	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.)
⊢ V ≠ ∅
Theorem	n0f 3559	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 3560 requires only that x not be free in, rather than not occur in, A. (Contributed by NM, 17-Oct-2003.)
⊢ ℲxA    ⇒   ⊢ (A ≠ ∅ ↔ ∃x x ∈ A)
Theorem	n0 3560*	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.)
⊢ (A ≠ ∅ ↔ ∃x x ∈ A)
Theorem	neq0 3561*	A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ A = ∅ ↔ ∃x x ∈ A)
Theorem	reximdva0 3562*	Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.)
⊢ ((φ ∧ x ∈ A) → ψ)    ⇒   ⊢ ((φ ∧ A ≠ ∅) → ∃x ∈ A ψ)
Theorem	n0moeu 3563*	A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.)
⊢ (A ≠ ∅ → (∃*x x ∈ A ↔ ∃!x x ∈ A))
Theorem	rex0 3564	Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.)
⊢ ¬ ∃x ∈ ∅ φ
Theorem	eq0 3565*	The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.)
⊢ (A = ∅ ↔ ∀x ¬ x ∈ A)
Theorem	eqv 3566*	The universe contains every set. (Contributed by NM, 11-Sep-2006.)
⊢ (A = V ↔ ∀x x ∈ A)
Theorem	0el 3567*	Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (∅ ∈ A ↔ ∃x ∈ A ∀y ¬ y ∈ x)
Theorem	abvor0 3568*	The class builder of a wff not containing the abstraction variable is either the universal class or the empty set. (Contributed by Mario Carneiro, 29-Aug-2013.)
⊢ ({x ∣ φ} = V ∨ {x ∣ φ} = ∅)
Theorem	abn0 3569	Nonempty class abstraction. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
⊢ ({x ∣ φ} ≠ ∅ ↔ ∃xφ)
Theorem	ab0 3570	Empty class abstraction. (Contributed by SF, 5-Jan-2018.)
⊢ ({x ∣ φ} = ∅ ↔ ∀x ¬ φ)
Theorem	rabn0 3571	Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.)
⊢ ({x ∈ A ∣ φ} ≠ ∅ ↔ ∃x ∈ A φ)
Theorem	rab0 3572	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.)
⊢ {x ∈ ∅ ∣ φ} = ∅
Theorem	rabeq0 3573	Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)
⊢ ({x ∈ A ∣ φ} = ∅ ↔ ∀x ∈ A ¬ φ)
Theorem	rabxm 3574*	Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ A = ({x ∈ A ∣ φ} ∪ {x ∈ A ∣ ¬ φ})
Theorem	rabnc 3575*	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ ({x ∈ A ∣ φ} ∩ {x ∈ A ∣ ¬ φ}) = ∅
Theorem	un0 3576	The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
⊢ (A ∪ ∅) = A
Theorem	in0 3577	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.)
⊢ (A ∩ ∅) = ∅
Theorem	inv1 3578	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.)
⊢ (A ∩ V) = A
Theorem	unv 3579	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.)
⊢ (A ∪ V) = V
Theorem	0ss 3580	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
⊢ ∅ ⊆ A
Theorem	ss0b 3581	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.)
⊢ (A ⊆ ∅ ↔ A = ∅)
Theorem	ss0 3582	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)
⊢ (A ⊆ ∅ → A = ∅)
Theorem	sseq0 3583	A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ((A ⊆ B ∧ B = ∅) → A = ∅)
Theorem	ssn0 3584	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
⊢ ((A ⊆ B ∧ A ≠ ∅) → B ≠ ∅)
Theorem	abf 3585	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
⊢ ¬ φ    ⇒   ⊢ {x ∣ φ} = ∅
Theorem	eq0rdv 3586*	Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
⊢ (φ → ¬ x ∈ A)    ⇒   ⊢ (φ → A = ∅)
Theorem	un00 3587	Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.)
⊢ ((A = ∅ ∧ B = ∅) ↔ (A ∪ B) = ∅)
Theorem	vss 3588	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 ⊆ A ↔ A = V)
Theorem	0pss 3589	The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.)
⊢ (∅ ⊊ A ↔ A ≠ ∅)
Theorem	npss0 3590	No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ ¬ A ⊊ ∅
Theorem	pssv 3591	Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.)
⊢ (A ⊊ V ↔ ¬ A = V)
Theorem	disj 3592*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.)
⊢ ((A ∩ B) = ∅ ↔ ∀x ∈ A ¬ x ∈ B)
Theorem	disjr 3593*	Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((A ∩ B) = ∅ ↔ ∀x ∈ B ¬ x ∈ A)
Theorem	disj1 3594*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)
⊢ ((A ∩ B) = ∅ ↔ ∀x(x ∈ A → ¬ x ∈ B))
Theorem	reldisj 3595	Two ways of saying that two classes are disjoint, using the complement of B relative to a universe C. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (A ⊆ C → ((A ∩ B) = ∅ ↔ A ⊆ (C ∖ B)))
Theorem	disj3 3596	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
⊢ ((A ∩ B) = ∅ ↔ A = (A ∖ B))
Theorem	disjne 3597	Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((A ∩ B) = ∅ ∧ C ∈ A ∧ D ∈ B) → C ≠ D)
Theorem	disjel 3598	A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.)
⊢ (((A ∩ B) = ∅ ∧ C ∈ A) → ¬ C ∈ B)
Theorem	disj2 3599	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
⊢ ((A ∩ B) = ∅ ↔ A ⊆ (V ∖ B))
Theorem	disj4 3600	Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.)
⊢ ((A ∩ B) = ∅ ↔ ¬ (A ∖ B) ⊊ A)