P. 36 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3501-3600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	abanssl 3501	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.)
|- { f | ( ph /\ ps ) } C_ { f | ph }
Theorem	abanssr 3502	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.)
|- { f | ( ph /\ ps ) } C_ { f | ps }
Theorem	notab 3503	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
|- { x | -. ph } = ( _V \ { x | ph } )
Theorem	unrab 3504	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 3505	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 3506*	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 3507	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 3508*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.)
|- { x e. A | ph } = ( { x | ph } i^i A )
Theorem	dfrab3 3509*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- { x e. A | ph } = ( A i^i { x | ph } )
Theorem	notrab 3510*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A \ { x e. A | ph } ) = { x e. A | -. ph }
Theorem	dfrab3ss 3511*	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 3512	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 } )
2.1.13.6  Restricted uniqueness with difference, union, and intersection
Theorem	reuss2 3513*	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 3514*	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 3515*	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 3516*	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 3517*	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 3518*	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 3519*	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 ) )
2.1.14  The empty set
Syntax	c0 3520	Extend class notation to include the empty set.
class (/)
Definition	df-nul 3521	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 3523. (Contributed by NM, 5-Aug-1993.)
|- (/) = ( _V \ _V )
Theorem	dfnul4 3522	Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) Avoid ax-13 2211, df-clel 2234. (Revised by GG, 3-Sep-2024.) Prove directly from definition to allow shortening dfnul2 3523. (Revised by BJ, 23-Sep-2024.)
|- (/) = { x | F. }
Theorem	dfnul2 3523	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Reduce axiom dependencies. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)
|- (/) = { x | -. x = x }
Theorem	dfnul3 3524	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) (Proof shortened by BJ, 23-Sep-2024.)
|- (/) = { x e. A | -. x e. A }
Theorem	noel 3525	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	nel02 3526	The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.)
|- ( A = (/) -> -. B e. A )
Theorem	n0i 3527	If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2838. (Contributed by NM, 31-Dec-1993.)
|- ( B e. A -> -. A = (/) )
Theorem	ne0i 3528	If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2838. (Contributed by NM, 31-Dec-1993.)
|- ( B e. A -> A =/= (/) )
Theorem	ne0d 3529	Deduction form of ne0i 3528. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> B e. A )   =>    |- ( ph -> A =/= (/) )
Theorem	n0ii 3530	If a class has elements, then it is not empty. Inference associated with n0i 3527. (Contributed by BJ, 15-Jul-2021.)
|- A e. B   =>    |- -. B = (/)
Theorem	ne0ii 3531	If a class has elements, then it is nonempty. Inference associated with ne0i 3528. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- A e. B   =>    |- B =/= (/)
Theorem	vn0 3532	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.)
|- _V =/= (/)
Theorem	vn0m 3533	The universal class is inhabited. (Contributed by Jim Kingdon, 17-Dec-2018.)
|- E. x x e. _V
Theorem	n0rf 3534	An inhabited class is nonempty. Following the Definition of [Bauer], p. 483, we call a class A nonempty if A =/= (/) 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 3535 requires only that x not be free in, rather than not occur in, A. (Contributed by Jim Kingdon, 31-Jul-2018.)
|- F/_ x A   =>    |- ( E. x x e. A -> A =/= (/) )
Theorem	n0r 3535*	An inhabited class is nonempty. See n0rf 3534 for more discussion. (Contributed by Jim Kingdon, 31-Jul-2018.)
|- ( E. x x e. A -> A =/= (/) )
Theorem	neq0r 3536*	An inhabited class is nonempty. See n0rf 3534 for more discussion. (Contributed by Jim Kingdon, 31-Jul-2018.)
|- ( E. x x e. A -> -. A = (/) )
Theorem	reximdva0m 3537*	Restricted existence deduced from inhabited class. (Contributed by Jim Kingdon, 31-Jul-2018.)
|- ( ( ph /\ x e. A ) -> ps )   =>    |- ( ( ph /\ E. x x e. A ) -> E. x e. A ps )
Theorem	n0mmoeu 3538*	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.)
|- ( E. x x e. A -> ( E* x x e. A <-> E! x x e. A ) )
Theorem	rex0 3539	Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.)
|- -. E. x e. (/) ph
Theorem	eq0 3540*	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 3541*	The universe contains every set. (Contributed by NM, 11-Sep-2006.)
|- ( A = _V <-> A. x x e. A )
Theorem	notm0 3542*	A class is not inhabited if and only if it is empty. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- ( -. E. x x e. A <-> A = (/) )
Theorem	nel0 3543*	From the general negation of membership in A, infer that A is the empty set. (Contributed by BJ, 6-Oct-2018.)
|- -. x e. A   =>    |- A = (/)
Theorem	0el 3544*	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	abvor0dc 3545*	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 ph -> ( { x | ph } = _V \/ { x | ph } = (/) ) )
Theorem	abn0r 3546	Nonempty class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|- ( E. x ph -> { x | ph } =/= (/) )
Theorem	abn0m 3547*	Inhabited class abstraction. (Contributed by Jim Kingdon, 8-Jul-2022.)
|- ( E. y y e. { x | ph } <-> E. x ph )
Theorem	rabn0r 3548	Nonempty restricted class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|- ( E. x e. A ph -> { x e. A | ph } =/= (/) )
Theorem	rabn0m 3549*	Inhabited restricted class abstraction. (Contributed by Jim Kingdon, 18-Sep-2018.)
|- ( E. y y e. { x e. A | ph } <-> E. x e. A ph )
Theorem	ab0w 3550*	The class of sets verifying a property is the empty class if and only if that property is a contradiction. (Contributed by GG, 3-Oct-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( { x | ph } = (/) <-> A. y -. ps )
Theorem	rab0 3551	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 3552	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	abeq0 3553	Condition for a class abstraction to be empty. (Contributed by Jim Kingdon, 12-Aug-2018.)
|- ( { x | ph } = (/) <-> A. x -. ph )
Theorem	rabxmdc 3554*	Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Jim Kingdon, 17-Jun-2026.)
|- ( A. x e. A DECID ph -> A = ( { x e. A | ph } u. { x e. A | -. ph } ) )
Theorem	rabnc 3555*	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 3556	The union of a class with the empty set is itself. Dual of inv1 3559. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- ( A u. (/) ) = A
Theorem	in0 3557	The intersection of a class with the empty set is the empty set. Dual of unv 3560. Commuted form of 0in 3558. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
|- ( A i^i (/) ) = (/)
Theorem	0in 3558	The intersection of the empty set with a class is the empty set. Commuted form of in0 3557. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( (/) i^i A ) = (/)
Theorem	inv1 3559	The intersection of a class with the universal class is itself. Dual of un0 3556. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.)
|- ( A i^i _V ) = A
Theorem	unv 3560	The union of a class with the universal class is the universal class. Dual of in0 3557. Exercise 4.10(l) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.)
|- ( A u. _V ) = _V
Theorem	0ss 3561	The empty set is a subset of any class. Dual of ssv 3270. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
|- (/) C_ A
Theorem	ss0b 3562	Any subset of the empty set is empty. Dual of vss 3567. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.)
|- ( A C_ (/) <-> A = (/) )
Theorem	ss0 3563	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 3564	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 3565	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
|- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )
Theorem	un00 3566	Two classes are both empty if and only if their union is empty. Dual of vvin 3568. (Contributed by NM, 11-Aug-2004.)
|- ( ( A = (/) /\ B = (/) ) <-> ( A u. B ) = (/) )
Theorem	vss 3567	Only the universal class has the universal class as a subclass. Dual of ss0b 3562. (Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( _V C_ A <-> A = _V )
Theorem	vvin 3568	Two classes are both the universal class if and only if their intersection is the universal class. Dual of un00 3566. (Contributed by BJ, 12-Jul-2026.)
|- ( ( A = _V /\ B = _V ) <-> ( A i^i B ) = _V )
Theorem	abf 3569	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
|- -. ph   =>    |- { x | ph } = (/)
Theorem	eq0rdv 3570*	Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
|- ( ph -> -. x e. A )   =>    |- ( ph -> A = (/) )
Theorem	csbprc 3571	The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.)
|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
Theorem	disj 3572*	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 3573*	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 3574*	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 3575	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 3576	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
|- ( ( A i^i B ) = (/) <-> A = ( A \ B ) )
Theorem	disjne 3577	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 3578	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 3579	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
|- ( ( A i^i B ) = (/) <-> A C_ ( _V \ B ) )
Theorem	ssdisj 3580	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.)
|- ( ( A C_ B /\ ( B i^i C ) = (/) ) -> ( A i^i C ) = (/) )
Theorem	undisj1 3581	The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
|- ( ( ( A i^i C ) = (/) /\ ( B i^i C ) = (/) ) <-> ( ( A u. B ) i^i C ) = (/) )
Theorem	undisj2 3582	The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
|- ( ( ( A i^i B ) = (/) /\ ( A i^i C ) = (/) ) <-> ( A i^i ( B u. C ) ) = (/) )
Theorem	ssindif0im 3583	Subclass implies empty intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
|- ( A C_ B -> ( A i^i ( _V \ B ) ) = (/) )
Theorem	inelcm 3584	The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
|- ( ( A e. B /\ A e. C ) -> ( B i^i C ) =/= (/) )
Theorem	minel 3585	A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.)
|- ( ( A e. B /\ ( C i^i B ) = (/) ) -> -. A e. C )
Theorem	undif4 3586	Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i C ) = (/) -> ( A u. ( B \ C ) ) = ( ( A u. B ) \ C ) )
Theorem	disjssun 3587	Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i B ) = (/) -> ( A C_ ( B u. C ) <-> A C_ C ) )
Theorem	ssdif0im 3588	Subclass implies empty difference. One direction of Exercise 7 of [TakeutiZaring] p. 22. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 2-Aug-2018.)
|- ( A C_ B -> ( A \ B ) = (/) )
Theorem	vdif0im 3589	Universal class equality in terms of empty difference. (Contributed by Jim Kingdon, 3-Aug-2018.)
|- ( A = _V -> ( _V \ A ) = (/) )
Theorem	difrab0eqim 3590*	If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Jim Kingdon, 3-Aug-2018.)
|- ( V = { x e. V | ph } -> ( V \ { x e. V | ph } ) = (/) )
Theorem	inssdif0im 3591	Intersection, subclass, and difference relationship. In classical logic the converse would also hold. (Contributed by Jim Kingdon, 3-Aug-2018.)
|- ( ( A i^i B ) C_ C -> ( A i^i ( B \ C ) ) = (/) )
Theorem	difid 3592	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.)
|- ( A \ A ) = (/)
Theorem	difidALT 3593	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. Alternate proof of difid 3592. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A \ A ) = (/)
Theorem	dif0 3594	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
|- ( A \ (/) ) = A
Theorem	0dif 3595	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
|- ( (/) \ A ) = (/)
Theorem	disjdif 3596	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)
|- ( A i^i ( B \ A ) ) = (/)
Theorem	disjdifr 3597	A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.)
|- ( ( B \ A ) i^i A ) = (/)
Theorem	difin0 3598	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i B ) \ B ) = (/)
Theorem	undif1ss 3599	Absorption of difference by union. In classical logic, as Theorem 35 of [Suppes] p. 29, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( A \ B ) u. B ) C_ ( A u. B )
Theorem	undif2ss 3600	Absorption of difference by union. In classical logic, as in Part of proof of Corollary 6K of [Enderton] p. 144, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( A u. ( B \ A ) ) C_ ( A u. B )