P. 34 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3301-3400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inss 3301	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
|- ( ( A C_ C \/ B C_ C ) -> ( A i^i B ) C_ C )
2.1.13.4  Combinations of difference, union, and intersection of two classes
Theorem	unabs 3302	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|- ( A u. ( A i^i B ) ) = A
Theorem	inabs 3303	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|- ( A i^i ( A u. B ) ) = A
Theorem	dfss4st 3304*	Subclass defined in terms of class difference. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A. xSTAB x e. A -> ( A C_ B <-> ( B \ ( B \ A ) ) = A ) )
Theorem	ssddif 3305	Double complement and subset. Similar to ddifss 3309 but inside a class B instead of the universal class _V. In classical logic the subset operation on the right hand side could be an equality (that is, A C_ B <-> ( B \ ( B \ A ) ) = A). (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A C_ B <-> A C_ ( B \ ( B \ A ) ) )
Theorem	unssdif 3306	Union of two classes and class difference. In classical logic this would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A u. B ) C_ ( _V \ ( ( _V \ A ) \ B ) )
Theorem	inssdif 3307	Intersection of two classes and class difference. In classical logic this would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A i^i B ) C_ ( A \ ( _V \ B ) )
Theorem	difin 3308	Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A \ ( A i^i B ) ) = ( A \ B )
Theorem	ddifss 3309	Double complement under universal class. In classical logic (or given an additional hypothesis, as in ddifnel 3202), this is equality rather than subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- A C_ ( _V \ ( _V \ A ) )
Theorem	unssin 3310	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.)
|- ( A u. B ) C_ ( _V \ ( ( _V \ A ) i^i ( _V \ B ) ) )
Theorem	inssun 3311	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.)
|- ( A i^i B ) C_ ( _V \ ( ( _V \ A ) u. ( _V \ B ) ) )
Theorem	inssddif 3312	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.)
|- ( A i^i B ) C_ ( A \ ( A \ B ) )
Theorem	invdif 3313	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( _V \ B ) ) = ( A \ B )
Theorem	indif 3314	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( A \ B ) ) = ( A \ B )
Theorem	indif2 3315	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
|- ( A i^i ( B \ C ) ) = ( ( A i^i B ) \ C )
Theorem	indif1 3316	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( A \ C ) i^i B ) = ( ( A i^i B ) \ C )
Theorem	indifcom 3317	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 3318	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 3319	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 3320	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 3321	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	uneqin 3322	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 3323	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 3324	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) \ C ) = ( ( A \ C ) u. ( B \ C ) )
Theorem	difindiss 3325	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.)
|- ( ( A \ B ) u. ( A \ C ) ) C_ ( A \ ( B i^i C ) )
Theorem	difindir 3326	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A i^i B ) \ C ) = ( ( A \ C ) i^i ( B \ C ) )
Theorem	indifdir 3327	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	difdif2ss 3328	Set difference with a set difference. In classical logic this would be equality rather than subset. (Contributed by Jim Kingdon, 27-Jul-2018.)
|- ( ( A \ B ) u. ( A i^i C ) ) C_ ( A \ ( B \ C ) )
Theorem	undm 3329	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	indmss 3330	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 \ A ) u. ( _V \ B ) ) C_ ( _V \ ( A i^i B ) )
Theorem	difun1 3331	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
|- ( A \ ( B u. C ) ) = ( ( A \ B ) \ C )
Theorem	undif3ss 3332	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.)
|- ( A u. ( B \ C ) ) C_ ( ( A u. B ) \ ( C \ A ) )
Theorem	difin2 3333	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 3334	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ B )
Theorem	difabs 3335	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 3336	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 ) )
2.1.13.5  Class abstractions with difference, union, and intersection of two classes
Theorem	symdifxor 3337*	Expressing symmetric difference with exclusive-or or two differences. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- ( ( A \ B ) u. ( B \ A ) ) = { x | ( x e. A \/_ x e. B ) }
Theorem	unab 3338	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 3339	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 3340	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	notab 3341	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
|- { x | -. ph } = ( _V \ { x | ph } )
Theorem	unrab 3342	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 3343	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 3344*	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 3345	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 3346*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.)
|- { x e. A | ph } = ( { x | ph } i^i A )
Theorem	dfrab3 3347*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- { x e. A | ph } = ( A i^i { x | ph } )
Theorem	notrab 3348*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A \ { x e. A | ph } ) = { x e. A | -. ph }
Theorem	dfrab3ss 3349*	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 3350	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 3351*	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 3352*	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 3353*	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 3354*	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 3355*	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 3356*	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 3357*	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 3358	Extend class notation to include the empty set.
class (/)
Definition	df-nul 3359	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 3360. (Contributed by NM, 5-Aug-1993.)
|- (/) = ( _V \ _V )
Theorem	dfnul2 3360	Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.)
|- (/) = { x | -. x = x }
Theorem	dfnul3 3361	Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.)
|- (/) = { x e. A | -. x e. A }
Theorem	noel 3362	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 3363	If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2697. (Contributed by NM, 31-Dec-1993.)
|- ( B e. A -> -. A = (/) )
Theorem	ne0i 3364	If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2697. (Contributed by NM, 31-Dec-1993.)
|- ( B e. A -> A =/= (/) )
Theorem	ne0d 3365	Deduction form of ne0i 3364. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> B e. A )   =>    |- ( ph -> A =/= (/) )
Theorem	n0ii 3366	If a class has elements, then it is not empty. Inference associated with n0i 3363. (Contributed by BJ, 15-Jul-2021.)
|- A e. B   =>    |- -. B = (/)
Theorem	ne0ii 3367	If a class has elements, then it is nonempty. Inference associated with ne0i 3364. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- A e. B   =>    |- B =/= (/)
Theorem	vn0 3368	The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.)
|- _V =/= (/)
Theorem	vn0m 3369	The universal class is inhabited. (Contributed by Jim Kingdon, 17-Dec-2018.)
|- E. x x e. _V
Theorem	n0rf 3370	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 3371 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 3371*	An inhabited class is nonempty. See n0rf 3370 for more discussion. (Contributed by Jim Kingdon, 31-Jul-2018.)
|- ( E. x x e. A -> A =/= (/) )
Theorem	neq0r 3372*	An inhabited class is nonempty. See n0rf 3370 for more discussion. (Contributed by Jim Kingdon, 31-Jul-2018.)
|- ( E. x x e. A -> -. A = (/) )
Theorem	reximdva0m 3373*	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 3374*	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 3375	Vacuous existential quantification is false. (Contributed by NM, 15-Oct-2003.)
|- -. E. x e. (/) ph
Theorem	eq0 3376*	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 3377*	The universe contains every set. (Contributed by NM, 11-Sep-2006.)
|- ( A = _V <-> A. x x e. A )
Theorem	notm0 3378*	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 3379*	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 3380*	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 3381*	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 3382	Nonempty class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|- ( E. x ph -> { x | ph } =/= (/) )
Theorem	abn0m 3383*	Inhabited class abstraction. (Contributed by Jim Kingdon, 8-Jul-2022.)
|- ( E. y y e. { x | ph } <-> E. x ph )
Theorem	rabn0r 3384	Nonempty restricted class abstraction. (Contributed by Jim Kingdon, 1-Aug-2018.)
|- ( E. x e. A ph -> { x e. A | ph } =/= (/) )
Theorem	rabn0m 3385*	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	rab0 3386	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 3387	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 3388	Condition for a class abstraction to be empty. (Contributed by Jim Kingdon, 12-Aug-2018.)
|- ( { x | ph } = (/) <-> A. x -. ph )
Theorem	rabxmdc 3389*	Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jim Kingdon, 2-Aug-2018.)
|- ( A. xDECID ph -> A = ( { x e. A | ph } u. { x e. A | -. ph } ) )
Theorem	rabnc 3390*	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 3391	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 3392	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	0in 3393	The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( (/) i^i A ) = (/)
Theorem	inv1 3394	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 3395	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 3396	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 3397	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 3398	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 3399	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 3400	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
|- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )