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	preq12i 3701	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   &    |- C = D   =>    |- { A , C } = { B , D }
Theorem	preq1d 3702	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C } = { B , C } )
Theorem	preq2d 3703	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A } = { C , B } )
Theorem	preq12d 3704	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> { A , C } = { B , D } )
Theorem	tpeq1 3705	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { A , C , D } = { B , C , D } )
Theorem	tpeq2 3706	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , A , D } = { C , B , D } )
Theorem	tpeq3 3707	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , D , A } = { C , D , B } )
Theorem	tpeq1d 3708	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C , D } = { B , C , D } )
Theorem	tpeq2d 3709	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A , D } = { C , B , D } )
Theorem	tpeq3d 3710	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , D , A } = { C , D , B } )
Theorem	tpeq123d 3711	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 3712	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
|- { A , B , C } = { B , C , A }
Theorem	tpcoma 3713	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { B , A , C }
Theorem	tpcomb 3714	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { A , C , B }
Theorem	tpass 3715	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 3716	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 3717	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 3718	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 3719	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 3720	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 3721	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 3722	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 3723	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 3724	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 3725	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 3726	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 3727	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
|- ( -. A e. _V -> { A , B } = { B } )
Theorem	prprc2 3728	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
|- ( -. B e. _V -> { A , B } = { A } )
Theorem	prprc 3729	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 3730	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 3731	Closed theorem form of tpid1 3730. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { A , C , D } )
Theorem	tpid2 3732	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 3733	Closed theorem form of tpid2 3732. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { C , A , D } )
Theorem	tpid3g 3734	Closed theorem form of tpid3 3735. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( A e. B -> A e. { C , D , A } )
Theorem	tpid3 3735	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 3736	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|- ( A e. V -> { A } =/= (/) )
Theorem	snmg 3737*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( A e. V -> E. x x e. { A } )
Theorem	snnz 3738	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A } =/= (/)
Theorem	snm 3739*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- A e. _V   =>    |- E. x x e. { A }
Theorem	prmg 3740*	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 3741	A pair containing a set is not empty. It is also inhabited (see prm 3742). (Contributed by NM, 9-Apr-1994.)
|- A e. _V   =>    |- { A , B } =/= (/)
Theorem	prm 3742*	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 3743	A pair containing a set is not empty. It is also inhabited (see prmg 3740). (Contributed by FL, 19-Sep-2011.)
|- ( A e. V -> { A , B } =/= (/) )
Theorem	tpnz 3744	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A , B , C } =/= (/)
Theorem	snssOLD 3745	Obsolete version of snss 3754 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 3746	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 3747	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 3748	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
|- ( A e. ( B \ { C } ) -> A =/= C )
Theorem	neldifsn 3749	A is not in ( B \ { A } ). (Contributed by David Moews, 1-May-2017.)
|- -. A e. ( B \ { A } )
Theorem	neldifsnd 3750	A is not in ( B \ { A } ). Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> -. A e. ( B \ { A } ) )
Theorem	rexdifsn 3751	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 3752	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 3753	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 3754	The singleton of an element of a class is a subset of the class (inference form of snssg 3753). 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 3755	Obsolete version of snssgOLD 3755 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 3756	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 3757	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 3758	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( A =/= B -> ( { A , B } \ { A } ) = { B } )
Theorem	difprsn2 3759	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 3760	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 3761	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 3762	( B \ { A } ) equals B if and only if A is not a member of B. Generalization of difsn 3756. (Contributed by David Moews, 1-May-2017.)
|- ( -. A e. B <-> ( B \ { A } ) = B )
Theorem	snssi 3763	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 3764	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 3765	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 6562. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( B e. A -> ( ( A \ { B } ) u. { B } ) C_ A )
Theorem	pw0 3766	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 3767	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
|- { A } C_ { A , B }
Theorem	snsspr2 3768	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
|- { B } C_ { A , B }
Theorem	snsstp1 3769	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 3770	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 3771	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 3772	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 3773	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 3774	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 3775	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 3776	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 3777	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 3778	Deduction version of prssi 3777: 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 3779	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 3780	Empty set and the singleton itself are subsets of a singleton. Concerning the converse, see exmidsssn 4232. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( ( A = (/) \/ A = { B } ) -> A C_ { B } )
Theorem	sssnm 3781*	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 3782*	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 3783	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 3784	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 3785	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 3786	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 3787	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 3788	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 3789	Closed form of sneqr 3787. (Contributed by Scott Fenton, 1-Apr-2011.)
|- ( A e. V -> ( { A } = { B } -> A = B ) )
Theorem	sneqbg 3790	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 3791	The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)
|- { A } C_ ~P A
Theorem	prsspw 3792	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 3793	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 3795. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { A , C } = { B , C } -> A = B ) )
Theorem	preqr2g 3794	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the second elements are equal. Closed form of preqr2 3796. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { C , A } = { C , B } -> A = B ) )
Theorem	preqr1 3795	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 3796	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 3797	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 3798	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 3799	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 3800	Closed form of preq12b 3797. (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 ) ) ) )