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 i^i (B \ C)) = (B i^i (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 i^i (B u. C)) = ((A i^i B) u. (A i^i 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 u. (B i^i C)) = ((A u. B) i^i (A u. C))
Theorem	indir 3504	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
|- ((A u. B) i^i C) = ((A i^i C) u. (B i^i C))
Theorem	undir 3505	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
|- ((A i^i B) u. C) = ((A u. C) i^i (B u. 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 u. C) = (B u. C) /\ (A i^i C) = (B i^i 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 u. B) = (A i^i 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 u. C)) = ((A \ B) i^i (A \ C))
Theorem	difundir 3509	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ((A u. B) \ C) = ((A \ C) u. (B \ C))
Theorem	difindi 3510	Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- (A \ (B i^i C)) = ((A \ B) u. (A \ C))
Theorem	difindir 3511	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ((A i^i B) \ C) = ((A \ C) i^i (B \ C))
Theorem	indifdir 3512	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.)
|- ((A \ B) i^i C) = ((A i^i C) \ (B i^i 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 u. B)) = ((_V \ A) i^i (_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 i^i B)) = ((_V \ A) u. (_V \ B))
Theorem	difun1 3515	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
|- (A \ (B u. 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 u. (B \ C)) = ((A u. 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_ C -> (A \ B) = ((C \ B) i^i 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) u. (B \ A)) = ((A u. B) \ (A i^i 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) u. (B \ A)) = {x | -. (x e. A <-> x e. B)}
Theorem	unab 3522	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ({x | ph} u. {x | ps}) = {x | (ph \/ ps)}
Theorem	inab 3523	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ({x | ph} i^i {x | ps}) = {x | (ph /\ ps)}
Theorem	difab 3524	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ({x | ph} \ {x | ps}) = {x | (ph /\ -. ps)}
Theorem	complab 3525	Complement of a class abstraction. (Contributed by SF, 12-Jan-2015.)
|- ∼ {x | ph} = {x | -. ph}
Theorem	notab 3526	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
|- {x | -. ph} = (_V \ {x | ph})
Theorem	unrab 3527	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
|- ({x e. A | ph} u. {x e. A | ps}) = {x e. A | (ph \/ ps)}
Theorem	inrab 3528	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
|- ({x e. A | ph} i^i {x e. A | ps}) = {x e. A | (ph /\ ps)}
Theorem	inrab2 3529*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
|- ({x e. A | ph} i^i B) = {x e. (A i^i B) | ph}
Theorem	difrab 3530	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
|- ({x e. A | ph} \ {x e. A | ps}) = {x e. A | (ph /\ -. ps)}
Theorem	dfrab2 3531*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.)
|- {x e. A | ph} = ({x | ph} i^i A)
Theorem	dfrab3 3532*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- {x e. A | ph} = (A i^i {x | ph})
Theorem	notrab 3533*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- (A \ {x e. A | ph}) = {x e. A | -. ph}
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 C_ B -> {x e. A | ph} = (A i^i {x e. B | ph}))
Theorem	rabun2 3535	Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.)
|- {x e. (A u. B) | ph} = ({x e. A | ph} u. {x e. B | ph})
Theorem	reuss2 3536*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
|- (((A C_ B /\ A.x e. A (ph -> ps)) /\ (E.x e. A ph /\ E!x e. B ps)) -> E!x e. A ph)
Theorem	reuss 3537*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
|- ((A C_ B /\ E.x e. A ph /\ E!x e. B ph) -> E!x e. A ph)
Theorem	reuun1 3538*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
|- ((E.x e. A ph /\ E!x e. (A u. B)(ph \/ ps)) -> E!x e. A ph)
Theorem	reuun2 3539*	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)
|- (-. E.x e. B ph -> (E!x e. (A u. B)ph <-> E!x e. A ph))
Theorem	reupick 3540*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
|- (((A C_ B /\ (E.x e. A ph /\ E!x e. B ph)) /\ ph) -> (x e. A <-> x e. B))
Theorem	reupick3 3541*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
|- ((E!x e. A ph /\ E.x e. A (ph /\ ps) /\ x e. A) -> (ph -> ps))
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.)
|- (((A.x e. A (ps -> ph) /\ E.x e. A ps /\ E!x e. A ph) /\ x e. A) -> (ph <-> ps))
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 i^i B) = ∼ ( ∼ A u. ∼ B)
Theorem	dfun4 3547	Definition of union in terms of intersection. (Contributed by SF, 12-Jan-2015.)
|- (A u. B) = ∼ ( ∼ A i^i ∼ B)
Theorem	iunin 3548	Intersection of two complements is equal to the complement of a union. (Contributed by SF, 12-Jan-2015.)
|- ∼ (A u. B) = ( ∼ A i^i ∼ B)
Theorem	iinun 3549	Complement of intersection is equal to union of complements. (Contributed by SF, 12-Jan-2015.)
|- ∼ (A i^i B) = ( ∼ A u. ∼ B)
Theorem	difsscompl 3550	A difference is a subset of the complement of its second argument. (Contributed by SF, 10-Mar-2015.)
|- (A \ B) C_ ∼ 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 e. A | -. x e. 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 e. (/)
Theorem	n0i 3556	If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)
|- (B e. A -> -. A = (/))
Theorem	ne0i 3557	If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)
|- (B e. 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.)
|- F/_xA   =>   |- (A =/= (/) <-> E.x x e. 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 =/= (/) <-> E.x x e. 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 = (/) <-> E.x x e. A)
Theorem	reximdva0 3562*	Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.)
|- ((ph /\ x e. A) -> ps)   =>   |- ((ph /\ A =/= (/)) -> E.x e. A ps)
Theorem	n0moeu 3563*	A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.)
|- (A =/= (/) -> (E*x x e. A <-> E!x x e. A))
Theorem	rex0 3564	Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.)
|- -. E.x e. (/) ph
Theorem	eq0 3565*	The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.)
|- (A = (/) <-> A.x -. x e. A)
Theorem	eqv 3566*	The universe contains every set. (Contributed by NM, 11-Sep-2006.)
|- (A = _V <-> A.x x e. A)
Theorem	0el 3567*	Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.)
|- ((/) e. A <-> E.x e. A A.y -. y e. 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 | ph} = _V \/ {x | ph} = (/))
Theorem	abn0 3569	Nonempty class abstraction. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|- ({x | ph} =/= (/) <-> E.xph)
Theorem	ab0 3570	Empty class abstraction. (Contributed by SF, 5-Jan-2018.)
|- ({x | ph} = (/) <-> A.x -. ph)
Theorem	rabn0 3571	Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.)
|- ({x e. A | ph} =/= (/) <-> E.x e. A ph)
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 e. (/) | ph} = (/)
Theorem	rabeq0 3573	Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)
|- ({x e. A | ph} = (/) <-> A.x e. A -. ph)
Theorem	rabxm 3574*	Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- A = ({x e. A | ph} u. {x e. A | -. ph})
Theorem	rabnc 3575*	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- ({x e. A | ph} i^i {x e. A | -. ph}) = (/)
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 u. (/)) = 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 i^i (/)) = (/)
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 i^i _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 u. _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.)
|- (/) C_ 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 C_ (/) <-> 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 C_ (/) -> 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 C_ B /\ B = (/)) -> A = (/))
Theorem	ssn0 3584	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
|- ((A C_ B /\ A =/= (/)) -> B =/= (/))
Theorem	abf 3585	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
|- -. ph   =>   |- {x | ph} = (/)
Theorem	eq0rdv 3586*	Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
|- (ph -> -. x e. A)   =>   |- (ph -> A = (/))
Theorem	un00 3587	Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.)
|- ((A = (/) /\ B = (/)) <-> (A u. 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 C_ A <-> A = _V)
Theorem	0pss 3589	The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.)
|- ((/) C. 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 C. (/)
Theorem	pssv 3591	Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.)
|- (A C. _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 i^i B) = (/) <-> A.x e. A -. x e. B)
Theorem	disjr 3593*	Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ((A i^i B) = (/) <-> A.x e. B -. x e. 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 i^i B) = (/) <-> A.x(x e. A -> -. x e. 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_ C -> ((A i^i B) = (/) <-> A C_ (C \ B)))
Theorem	disj3 3596	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
|- ((A i^i 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 i^i B) = (/) /\ C e. A /\ D e. B) -> C =/= D)
Theorem	disjel 3598	A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.)
|- (((A i^i B) = (/) /\ C e. A) -> -. C e. B)
Theorem	disj2 3599	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
|- ((A i^i B) = (/) <-> A C_ (_V \ B))
Theorem	disj4 3600	Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.)
|- ((A i^i B) = (/) <-> -. (A \ B) C. A)