P. 38 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3701-3800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	preq1d 3701	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C } = { B , C } )
Theorem	preq2d 3702	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A } = { C , B } )
Theorem	preq12d 3703	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> { A , C } = { B , D } )
Theorem	tpeq1 3704	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { A , C , D } = { B , C , D } )
Theorem	tpeq2 3705	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , A , D } = { C , B , D } )
Theorem	tpeq3 3706	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , D , A } = { C , D , B } )
Theorem	tpeq1d 3707	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C , D } = { B , C , D } )
Theorem	tpeq2d 3708	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A , D } = { C , B , D } )
Theorem	tpeq3d 3709	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , D , A } = { C , D , B } )
Theorem	tpeq123d 3710	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   &    |- ( ph -> E = F )   =>    |- ( ph -> { A , C , E } = { B , D , F } )
Theorem	tprot 3711	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
|- { A , B , C } = { B , C , A }
Theorem	tpcoma 3712	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { B , A , C }
Theorem	tpcomb 3713	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { A , C , B }
Theorem	tpass 3714	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- { A , B , C } = ( { A } u. { B , C } )
Theorem	qdass 3715	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- ( { A , B } u. { C , D } ) = ( { A , B , C } u. { D } )
Theorem	qdassr 3716	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- ( { A , B } u. { C , D } ) = ( { A } u. { B , C , D } )
Theorem	tpidm12 3717	Unordered triple { A , A , B } is just an overlong way to write { A , B }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , A , B } = { A , B }
Theorem	tpidm13 3718	Unordered triple { A , B , A } is just an overlong way to write { A , B }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , B , A } = { A , B }
Theorem	tpidm23 3719	Unordered triple { A , B , B } is just an overlong way to write { A , B }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , B , B } = { A , B }
Theorem	tpidm 3720	Unordered triple { A , A , A } is just an overlong way to write { A }. (Contributed by David A. Wheeler, 10-May-2015.)
|- { A , A , A } = { A }
Theorem	tppreq3 3721	An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
|- ( B = C -> { A , B , C } = { A , B } )
Theorem	prid1g 3722	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- ( A e. V -> A e. { A , B } )
Theorem	prid2g 3723	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- ( B e. V -> B e. { A , B } )
Theorem	prid1 3724	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- A e. { A , B }
Theorem	prid2 3725	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
|- B e. _V   =>    |- B e. { A , B }
Theorem	prprc1 3726	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
|- ( -. A e. _V -> { A , B } = { B } )
Theorem	prprc2 3727	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
|- ( -. B e. _V -> { A , B } = { A } )
Theorem	prprc 3728	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
|- ( ( -. A e. _V /\ -. B e. _V ) -> { A , B } = (/) )
Theorem	tpid1 3729	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   =>    |- A e. { A , B , C }
Theorem	tpid1g 3730	Closed theorem form of tpid1 3729. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { A , C , D } )
Theorem	tpid2 3731	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- B e. _V   =>    |- B e. { A , B , C }
Theorem	tpid2g 3732	Closed theorem form of tpid2 3731. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { C , A , D } )
Theorem	tpid3g 3733	Closed theorem form of tpid3 3734. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( A e. B -> A e. { C , D , A } )
Theorem	tpid3 3734	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- C e. _V   =>    |- C e. { A , B , C }
Theorem	snnzg 3735	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|- ( A e. V -> { A } =/= (/) )
Theorem	snmg 3736*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( A e. V -> E. x x e. { A } )
Theorem	snnz 3737	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A } =/= (/)
Theorem	snm 3738*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- A e. _V   =>    |- E. x x e. { A }
Theorem	prmg 3739*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( A e. V -> E. x x e. { A , B } )
Theorem	prnz 3740	A pair containing a set is not empty. It is also inhabited (see prm 3741). (Contributed by NM, 9-Apr-1994.)
|- A e. _V   =>    |- { A , B } =/= (/)
Theorem	prm 3741*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- A e. _V   =>    |- E. x x e. { A , B }
Theorem	prnzg 3742	A pair containing a set is not empty. It is also inhabited (see prmg 3739). (Contributed by FL, 19-Sep-2011.)
|- ( A e. V -> { A , B } =/= (/) )
Theorem	tpnz 3743	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A , B , C } =/= (/)
Theorem	snssOLD 3744	Obsolete version of snss 3753 as of 1-Jan-2025. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A e. _V   =>    |- ( A e. B <-> { A } C_ B )
Theorem	eldifsn 3745	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
|- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )
Theorem	ssdifsn 3746	Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
|- ( A C_ ( B \ { C } ) <-> ( A C_ B /\ -. C e. A ) )
Theorem	eldifsni 3747	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
|- ( A e. ( B \ { C } ) -> A =/= C )
Theorem	neldifsn 3748	A is not in ( B \ { A } ). (Contributed by David Moews, 1-May-2017.)
|- -. A e. ( B \ { A } )
Theorem	neldifsnd 3749	A is not in ( B \ { A } ). Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> -. A e. ( B \ { A } ) )
Theorem	rexdifsn 3750	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
|- ( E. x e. ( A \ { B } ) ph <-> E. x e. A ( x =/= B /\ ph ) )
Theorem	snssb 3751	Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.)
|- ( { A } C_ B <-> ( A e. _V -> A e. B ) )
Theorem	snssg 3752	The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)
|- ( A e. V -> ( A e. B <-> { A } C_ B ) )
Theorem	snss 3753	The singleton of an element of a class is a subset of the class (inference form of snssg 3752). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.)
|- A e. _V   =>    |- ( A e. B <-> { A } C_ B )
Theorem	snssgOLD 3754	Obsolete version of snssgOLD 3754 as of 1-Jan-2025. (Contributed by NM, 22-Jul-2001.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. V -> ( A e. B <-> { A } C_ B ) )
Theorem	difsn 3755	An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( -. A e. B -> ( B \ { A } ) = B )
Theorem	difprsnss 3756	Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( { A , B } \ { A } ) C_ { B }
Theorem	difprsn1 3757	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( A =/= B -> ( { A , B } \ { A } ) = { B } )
Theorem	difprsn2 3758	Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
|- ( A =/= B -> ( { A , B } \ { B } ) = { A } )
Theorem	diftpsn3 3759	Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
|- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
Theorem	difpr 3760	Removing two elements as pair of elements corresponds to removing each of the two elements as singletons. (Contributed by Alexander van der Vekens, 13-Jul-2018.)
|- ( A \ { B , C } ) = ( ( A \ { B } ) \ { C } )
Theorem	difsnb 3761	( B \ { A } ) equals B if and only if A is not a member of B. Generalization of difsn 3755. (Contributed by David Moews, 1-May-2017.)
|- ( -. A e. B <-> ( B \ { A } ) = B )
Theorem	snssi 3762	The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
|- ( A e. B -> { A } C_ B )
Theorem	snssd 3763	The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A e. B )   =>    |- ( ph -> { A } C_ B )
Theorem	difsnss 3764	If we remove a single element from a class then put it back in, we end up with a subset of the original class. If equality is decidable, we can replace subset with equality as seen in nndifsnid 6560. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( B e. A -> ( ( A \ { B } ) u. { B } ) C_ A )
Theorem	pw0 3765	Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ~P (/) = { (/) }
Theorem	snsspr1 3766	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
|- { A } C_ { A , B }
Theorem	snsspr2 3767	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
|- { B } C_ { A , B }
Theorem	snsstp1 3768	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- { A } C_ { A , B , C }
Theorem	snsstp2 3769	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- { B } C_ { A , B , C }
Theorem	snsstp3 3770	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- { C } C_ { A , B , C }
Theorem	prsstp12 3771	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- { A , B } C_ { A , B , C }
Theorem	prsstp13 3772	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- { A , C } C_ { A , B , C }
Theorem	prsstp23 3773	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- { B , C } C_ { A , B , C }
Theorem	prss 3774	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A e. C /\ B e. C ) <-> { A , B } C_ C )
Theorem	prssg 3775	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 22-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )
Theorem	prssi 3776	A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
|- ( ( A e. C /\ B e. C ) -> { A , B } C_ C )
Theorem	prssd 3777	Deduction version of prssi 3776: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. C )   =>    |- ( ph -> { A , B } C_ C )
Theorem	prsspwg 3778	An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by Thierry Arnoux, 3-Oct-2016.) (Revised by NM, 18-Jan-2018.)
|- ( ( A e. V /\ B e. W ) -> ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) ) )
Theorem	sssnr 3779	Empty set and the singleton itself are subsets of a singleton. Concerning the converse, see exmidsssn 4231. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( ( A = (/) \/ A = { B } ) -> A C_ { B } )
Theorem	sssnm 3780*	The inhabited subset of a singleton. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( E. x x e. A -> ( A C_ { B } <-> A = { B } ) )
Theorem	eqsnm 3781*	Two ways to express that an inhabited set equals a singleton. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( E. x x e. A -> ( A = { B } <-> A. x e. A x = B ) )
Theorem	ssprr 3782	The subsets of a pair. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) -> A C_ { B , C } )
Theorem	sstpr 3783	The subsets of a triple. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) \/ ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) ) -> A C_ { B , C , D } )
Theorem	tpss 3784	A triplet of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D )
Theorem	tpssi 3785	A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
|- ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B , C } C_ D )
Theorem	sneqr 3786	If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 27-Aug-1993.)
|- A e. _V   =>    |- ( { A } = { B } -> A = B )
Theorem	snsssn 3787	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
|- A e. _V   =>    |- ( { A } C_ { B } -> A = B )
Theorem	sneqrg 3788	Closed form of sneqr 3786. (Contributed by Scott Fenton, 1-Apr-2011.)
|- ( A e. V -> ( { A } = { B } -> A = B ) )
Theorem	sneqbg 3789	Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
|- ( A e. V -> ( { A } = { B } <-> A = B ) )
Theorem	snsspw 3790	The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)
|- { A } C_ ~P A
Theorem	prsspw 3791	An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) )
Theorem	preqr1g 3792	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 3794. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { A , C } = { B , C } -> A = B ) )
Theorem	preqr2g 3793	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the second elements are equal. Closed form of preqr2 3795. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { C , A } = { C , B } -> A = B ) )
Theorem	preqr1 3794	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A , C } = { B , C } -> A = B )
Theorem	preqr2 3795	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   &    |- B e. _V   =>    |- ( { C , A } = { C , B } -> A = B )
Theorem	preq12b 3796	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
Theorem	prel12 3797	Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( -. A = B -> ( { A , B } = { C , D } <-> ( A e. { C , D } /\ B e. { C , D } ) ) )
Theorem	opthpr 3798	A way to represent ordered pairs using unordered pairs with distinct members. (Contributed by NM, 27-Mar-2007.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( A =/= D -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )
Theorem	preq12bg 3799	Closed form of preq12b 3796. (Contributed by Scott Fenton, 28-Mar-2014.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
Theorem	prneimg 3800	Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) -> { A , B } =/= { C , D } ) )