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.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {A, C} = {B, C})
Theorem	preq2d 3807	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {C, A} = {C, B})
Theorem	preq12d 3808	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    ⇒   ⊢ (φ → {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.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {A, C, D} = {B, C, D})
Theorem	tpeq2d 3813	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {C, A, D} = {C, B, D})
Theorem	tpeq3d 3814	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → {C, D, A} = {C, D, B})
Theorem	tpeq123d 3815	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
⊢ (φ → A = B)    &   ⊢ (φ → C = D)    &   ⊢ (φ → E = F)    ⇒   ⊢ (φ → {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} ∪ {B, C})
Theorem	qdass 3820	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({A, B} ∪ {C, D}) = ({A, B, C} ∪ {D})
Theorem	qdassr 3821	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ ({A, B} ∪ {C, D}) = ({A} ∪ {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 ∈ V → A ∈ {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 ∈ V → B ∈ {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 ∈ V    ⇒   ⊢ A ∈ {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 ∈ V    ⇒   ⊢ B ∈ {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 ∈ V    ⇒   ⊢ A ∈ {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 ∈ V    ⇒   ⊢ B ∈ {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 ∈ B → A ∈ {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 ∈ V    ⇒   ⊢ C ∈ {A, B, C}
Theorem	snnzg 3834	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
⊢ (A ∈ V → {A} ≠ ∅)
Theorem	snnz 3835	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ A ∈ V    ⇒   ⊢ {A} ≠ ∅
Theorem	prnz 3836	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
⊢ A ∈ V    ⇒   ⊢ {A, B} ≠ ∅
Theorem	prnzg 3837	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
⊢ (A ∈ V → {A, B} ≠ ∅)
Theorem	tpnz 3838	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
⊢ A ∈ 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 ∈ V    ⇒   ⊢ (A ∈ B ↔ {A} ⊆ B)
Theorem	eldifsn 3840	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
⊢ (A ∈ (B ∖ {C}) ↔ (A ∈ B ∧ A ≠ C))
Theorem	eldifsni 3841	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
⊢ (A ∈ (B ∖ {C}) → A ≠ C)
Theorem	neldifsn 3842	A is not in (B ∖ {A}). (Contributed by David Moews, 1-May-2017.)
⊢ ¬ A ∈ (B ∖ {A})
Theorem	neldifsnd 3843	A is not in (B ∖ {A}). Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → ¬ A ∈ (B ∖ {A}))
Theorem	rexdifsn 3844	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
⊢ (∃x ∈ (A ∖ {B})φ ↔ ∃x ∈ A (x ≠ B ∧ φ))
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 ∈ V → (A ∈ B ↔ {A} ⊆ 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 ∈ 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}) ⊆ {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 ∈ 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 ∈ B ↔ (B ∖ {A}) ⊊ 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 ∈ B → {A} ⊆ 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.)
⊢ (φ → A ∈ B)    ⇒   ⊢ (φ → {A} ⊆ 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 ∈ A → ((A ∖ {B}) ∪ {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.)
⊢ ℘{∅} = {∅, {∅}}
Theorem	snsspr1 3857	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
⊢ {A} ⊆ {A, B}
Theorem	snsspr2 3858	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
⊢ {B} ⊆ {A, B}
Theorem	snsstp1 3859	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
⊢ {A} ⊆ {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} ⊆ {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} ⊆ {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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((A ∈ C ∧ B ∈ C) ↔ {A, B} ⊆ 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 ∈ V ∧ B ∈ W) → ((A ∈ C ∧ B ∈ C) ↔ {A, B} ⊆ C))
Theorem	prssi 3864	A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
⊢ ((A ∈ C ∧ B ∈ C) → {A, B} ⊆ C)
Theorem	sssn 3865	The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
⊢ (A ⊆ {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 ⊆ A ∧ A ⊆ (C ∪ {D})) ↔ ((B ⊆ A ∧ A ⊆ C) ∨ ((B ∪ {D}) ⊆ A ∧ A ⊆ (C ∪ {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 ⊆ A ∧ A ⊆ (B ∪ {C})) ↔ (A = B ∨ A = (B ∪ {C})))
Theorem	eqsn 3868*	Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.)
⊢ (A ≠ ∅ → (A = {B} ↔ ∀x ∈ 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 ⊆ A ∧ A ⊆ (B ∪ {C, D})) ↔ ((A = B ∨ A = (B ∪ {C})) ∨ (A = (B ∪ {D}) ∨ A = (B ∪ {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 ⊆ {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 ⊆ {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 ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ((A ∈ D ∧ B ∈ D ∧ C ∈ D) ↔ {A, B, 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 ∈ 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 ∈ V    ⇒   ⊢ ({A} ⊆ {B} → A = B)
Theorem	sneqrg 3875	Closed form of sneqr 3873. (Contributed by Scott Fenton, 1-Apr-2011.)
⊢ (A ∈ 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 ∈ V → ({A} = {B} ↔ A = B))
Theorem	sneqb 3877	Biconditional equality for singletons. (Contributed by SF, 14-Jan-2015.)
⊢ A ∈ 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} ⊆ ℘A
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 ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ({A, B} ⊆ ℘C ↔ (A ⊆ C ∧ B ⊆ 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 → (φ ↔ ψ))    ⇒   ⊢ (B ∈ C → (∀x ∈ (A ∪ {B})φ ↔ (∀x ∈ A φ ∧ ψ)))
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 → (φ ↔ χ))    &   ⊢ (y = B → (φ ↔ ψ))    &   ⊢ (x = B → (ψ ↔ θ))    ⇒   ⊢ (B ∈ C → (∀x ∈ (A ∪ {B})∀y ∈ (A ∪ {B})φ ↔ ((∀x ∈ A ∀y ∈ A φ ∧ ∀x ∈ A ψ) ∧ (∀y ∈ A χ ∧ θ))))
Theorem	pwsn 3882	The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
⊢ ℘{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.)
⊢ ℘{A} = {∅, {A}}
Theorem	pwpr 3884	The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
⊢ ℘{A, B} = ({∅, {A}} ∪ {{B}, {A, B}})
Theorem	pwtp 3885	The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
⊢ ℘{A, B, C} = (({∅, {A}} ∪ {{B}, {A, B}}) ∪ ({{C}, {A, C}} ∪ {{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.)
⊢ ℘{∅, {∅}} = ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}})
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.)
⊢ ℘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 ∈ V    ⇒   ⊢ ((A ∪ {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 ⊊ B ↔ (A ⊆ B ∧ ∃x ∈ B ¬ x ∈ A))
Theorem	adj11 3890	Adjoining a new element is one-to-one. (Contributed by SF, 29-Jan-2015.)
⊢ ((¬ C ∈ A ∧ ¬ C ∈ B) → ((A ∪ {C}) = (B ∪ {C}) ↔ A = B))
Theorem	disj5 3891	Two ways of saying that two classes are disjoint. (Contributed by SF, 5-Feb-2015.)
⊢ ((A ∩ B) = ∅ ↔ A ⊆ ∼ 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 ∪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, ∪{{ 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.)
⊢ ∪A = {x ∣ ∃y(x ∈ y ∧ y ∈ A)}
Theorem	dfuni2 3894*	Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
⊢ ∪A = {x ∣ ∃y ∈ A x ∈ y}
Theorem	eluni 3895*	Membership in class union. (Contributed by NM, 22-May-1994.)
⊢ (A ∈ ∪B ↔ ∃x(A ∈ x ∧ x ∈ B))
Theorem	eluni2 3896*	Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
⊢ (A ∈ ∪B ↔ ∃x ∈ B A ∈ x)
Theorem	elunii 3897	Membership in class union. (Contributed by NM, 24-Mar-1995.)
⊢ ((A ∈ B ∧ B ∈ C) → A ∈ ∪C)
Theorem	nfuni 3898	Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ℲxA    ⇒   ⊢ Ⅎx∪A
Theorem	nfunid 3899	Deduction version of nfuni 3898. (Contributed by NM, 18-Feb-2013.)
⊢ (φ → ℲxA)    ⇒   ⊢ (φ → Ⅎx∪A)
Theorem	csbunig 3900	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
⊢ (A ∈ V → [A / x]∪B = ∪[A / x]B)