P. 39 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 3801-3900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	preq2 3801	Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|- (A = B -> {C, A} = {C, B})
Theorem	preq12 3802	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ((A = C /\ B = D) -> {A, B} = {C, D})
Theorem	preq1i 3803	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>   |- {A, C} = {B, C}
Theorem	preq2i 3804	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>   |- {C, A} = {C, B}
Theorem	preq12i 3805	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   &   |- C = D   =>   |- {A, C} = {B, D}
Theorem	preq1d 3806	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- (ph -> A = B)   =>   |- (ph -> {A, C} = {B, C})
Theorem	preq2d 3807	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- (ph -> A = B)   =>   |- (ph -> {C, A} = {C, B})
Theorem	preq12d 3808	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> {A, C} = {B, D})
Theorem	tpeq1 3809	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- (A = B -> {A, C, D} = {B, C, D})
Theorem	tpeq2 3810	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- (A = B -> {C, A, D} = {C, B, D})
Theorem	tpeq3 3811	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- (A = B -> {C, D, A} = {C, D, B})
Theorem	tpeq1d 3812	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- (ph -> A = B)   =>   |- (ph -> {A, C, D} = {B, C, D})
Theorem	tpeq2d 3813	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- (ph -> A = B)   =>   |- (ph -> {C, A, D} = {C, B, D})
Theorem	tpeq3d 3814	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- (ph -> A = B)   =>   |- (ph -> {C, D, A} = {C, D, B})
Theorem	tpeq123d 3815	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 3816	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
|- {A, B, C} = {B, C, A}
Theorem	tpcoma 3817	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- {A, B, C} = {B, A, C}
Theorem	tpcomb 3818	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- {A, B, C} = {A, C, B}
Theorem	tpass 3819	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 3820	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 3821	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 3822	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 3823	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 3824	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 3825	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	prid1g 3826	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 3827	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 3828	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 3829	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	tpid1 3830	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	tpid2 3831	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	tpid3g 3832	Closed theorem form of tpid3 3833. This proof was automatically generated from the virtual deduction proof tpid3gVD in set.mm using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
|- (A e. B -> A e. {C, D, A})
Theorem	tpid3 3833	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 3834	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|- (A e. V -> {A} =/= (/))
Theorem	snnz 3835	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>   |- {A} =/= (/)
Theorem	prnz 3836	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
|- A e. _V   =>   |- {A, B} =/= (/)
Theorem	prnzg 3837	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
|- (A e. V -> {A, B} =/= (/))
Theorem	tpnz 3838	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>   |- {A, B, C} =/= (/)
Theorem	snss 3839	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>   |- (A e. B <-> {A} C_ B)
Theorem	eldifsn 3840	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
|- (A e. (B \ {C}) <-> (A e. B /\ A =/= C))
Theorem	eldifsni 3841	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
|- (A e. (B \ {C}) -> A =/= C)
Theorem	neldifsn 3842	A is not in (B \ {A}). (Contributed by David Moews, 1-May-2017.)
|- -. A e. (B \ {A})
Theorem	neldifsnd 3843	A is not in (B \ {A}). Deduction form. (Contributed by David Moews, 1-May-2017.)
|- (ph -> -. A e. (B \ {A}))
Theorem	rexdifsn 3844	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	snssg 3845	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
|- (A e. V -> (A e. B <-> {A} C_ B))
Theorem	difsn 3846	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 3847	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 3848	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- (A =/= B -> ({A, B} \ {A}) = {B})
Theorem	difprsn2 3849	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 3850	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	difsnb 3851	(B \ {A}) equals B if and only if A is not a member of B. Generalization of difsn 3846. (Contributed by David Moews, 1-May-2017.)
|- (-. A e. B <-> (B \ {A}) = B)
Theorem	difsnpss 3852	(B \ {A}) is a proper subclass of B if and only if A is a member of B. (Contributed by David Moews, 1-May-2017.)
|- (A e. B <-> (B \ {A}) C. B)
Theorem	snssi 3853	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 3854	The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> A e. B)   =>   |- (ph -> {A} C_ B)
Theorem	difsnid 3855	If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006.)
|- (B e. A -> ((A \ {B}) u. {B}) = A)
Theorem	pwpw0 3856	Compute the power set of the power set of the empty set. (See pw0 4161 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 3882, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.)
|- ~P{(/)} = {(/), {(/)}}
Theorem	snsspr1 3857	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
|- {A} C_ {A, B}
Theorem	snsspr2 3858	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
|- {B} C_ {A, B}
Theorem	snsstp1 3859	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 3860	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 3861	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- {C} C_ {A, B, C}
Theorem	prss 3862	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 3863	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 3864	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	sssn 3865	The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
|- (A C_ {B} <-> (A = (/) \/ A = {B}))
Theorem	ssunsn2 3866	The property of being sandwiched between two sets naturally splits under union with a singleton. This is the induction hypothesis for the determination of large powersets such as pwtp 3885. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ((B C_ A /\ A C_ (C u. {D})) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D}))))
Theorem	ssunsn 3867	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ((B C_ A /\ A C_ (B u. {C})) <-> (A = B \/ A = (B u. {C})))
Theorem	eqsn 3868*	Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.)
|- (A =/= (/) -> (A = {B} <-> A.x e. A x = B))
Theorem	ssunpr 3869	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ((B C_ A /\ A C_ (B u. {C, D})) <-> ((A = B \/ A = (B u. {C})) \/ (A = (B u. {D}) \/ A = (B u. {C, D}))))
Theorem	sspr 3870	The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.)
|- (A C_ {B, C} <-> ((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})))
Theorem	sstp 3871	The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- (A C_ {B, C, D} <-> (((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})) \/ ((A = {D} \/ A = {B, D}) \/ (A = {C, D} \/ A = {B, C, D}))))
Theorem	tpss 3872	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	sneqr 3873	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 3874	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 3875	Closed form of sneqr 3873. (Contributed by Scott Fenton, 1-Apr-2011.)
|- (A e. V -> ({A} = {B} -> A = B))
Theorem	sneqbg 3876	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	sneqb 3877	Biconditional equality for singletons. (Contributed by SF, 14-Jan-2015.)
|- A e. _V   =>   |- ({A} = {B} <-> A = B)
Theorem	snsspw 3878	The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)
|- {A} C_ ~PA
Theorem	prsspw 3879	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_ ~PC <-> (A C_ C /\ B C_ C))
Theorem	ralunsn 3880*	Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- (x = B -> (ph <-> ps))   =>   |- (B e. C -> (A.x e. (A u. {B})ph <-> (A.x e. A ph /\ ps)))
Theorem	2ralunsn 3881*	Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
|- (x = B -> (ph <-> ch))   &   |- (y = B -> (ph <-> ps))   &   |- (x = B -> (ps <-> th))   =>   |- (B e. C -> (A.x e. (A u. {B})A.y e. (A u. {B})ph <-> ((A.x e. A A.y e. A ph /\ A.x e. A ps) /\ (A.y e. A ch /\ th))))
Theorem	pwsn 3882	The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
|- ~P{A} = {(/), {A}}
Theorem	pwsnALT 3883	The power set of a singleton (direct proof). TO DO - should we keep this? (Contributed by NM, 5-Jun-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ~P{A} = {(/), {A}}
Theorem	pwpr 3884	The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
|- ~P{A, B} = ({(/), {A}} u. {{B}, {A, B}})
Theorem	pwtp 3885	The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ~P{A, B, C} = (({(/), {A}} u. {{B}, {A, B}}) u. ({{C}, {A, C}} u. {{B, C}, {A, B, C}}))
Theorem	pwpwpw0 3886	Compute the power set of the power set of the power set of the empty set. (See also pw0 4161 and pwpw0 3856.) (Contributed by NM, 2-May-2009.)
|- ~P{(/), {(/)}} = ({(/), {(/)}} u. {{{(/)}}, {(/), {(/)}}})
Theorem	pwv 3887	The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
|- ~P_V = _V
Theorem	unsneqsn 3888	If union with a singleton yields a singleton, then the first argument is either also the singleton or is the empty set. (Contributed by SF, 15-Jan-2015.)
|- B e. _V   =>   |- ((A u. {B}) = {C} -> (A = (/) \/ A = {B}))
Theorem	dfpss4 3889*	Alternate definition of proper subset. Theorem IX.4.21 of [Rosser] p. 236. (Contributed by SF, 19-Jan-2015.)
|- (A C. B <-> (A C_ B /\ E.x e. B -. x e. A))
Theorem	adj11 3890	Adjoining a new element is one-to-one. (Contributed by SF, 29-Jan-2015.)
|- ((-. C e. A /\ -. C e. B) -> ((A u. {C}) = (B u. {C}) <-> A = B))
Theorem	disj5 3891	Two ways of saying that two classes are disjoint. (Contributed by SF, 5-Feb-2015.)
|- ((A i^i B) = (/) <-> A C_ ∼ B)
2.1.17  The union of a class
Syntax	cuni 3892	Extend class notation to include the union of a class (read: 'union A')
class U.A
Definition	df-uni 3893*	Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, U.{{ 1 , 3 }, { 1 , 8 }} = { 1 , 3 , 8 } (ex-uni in set.mm). This is similar to the union of two classes df-un 3215. (Contributed by NM, 23-Aug-1993.)
|- U.A = {x | E.y(x e. y /\ y e. A)}
Theorem	dfuni2 3894*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
|- U.A = {x | E.y e. A x e. y}
Theorem	eluni 3895*	Membership in class union. (Contributed by NM, 22-May-1994.)
|- (A e. U.B <-> E.x(A e. x /\ x e. B))
Theorem	eluni2 3896*	Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
|- (A e. U.B <-> E.x e. B A e. x)
Theorem	elunii 3897	Membership in class union. (Contributed by NM, 24-Mar-1995.)
|- ((A e. B /\ B e. C) -> A e. U.C)
Theorem	nfuni 3898	Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- F/_xA   =>   |- F/_xU.A
Theorem	nfunid 3899	Deduction version of nfuni 3898. (Contributed by NM, 18-Feb-2013.)
|- (ph -> F/_xA)   =>   |- (ph -> F/_xU.A)
Theorem	csbunig 3900	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- (A e. V -> [_A / x]_U.B = U.[_A / x]_B)