Home New Foundations ExplorerTheorem List (p. 39 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

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

Theorempreq12 3801 Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
((A = C B = D) → {A, B} = {C, D})

Theorempreq1i 3802 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
A = B       {A, C} = {B, C}

Theorempreq2i 3803 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
A = B       {C, A} = {C, B}

Theorempreq12i 3804 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
A = B    &   C = D       {A, C} = {B, D}

Theorempreq1d 3805 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(φA = B)       (φ → {A, C} = {B, C})

Theorempreq2d 3806 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(φA = B)       (φ → {C, A} = {C, B})

Theorempreq12d 3807 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(φA = B)    &   (φC = D)       (φ → {A, C} = {B, D})

Theoremtpeq1 3808 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(A = B → {A, C, D} = {B, C, D})

Theoremtpeq2 3809 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(A = B → {C, A, D} = {C, B, D})

Theoremtpeq3 3810 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(A = B → {C, D, A} = {C, D, B})

Theoremtpeq1d 3811 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)       (φ → {A, C, D} = {B, C, D})

Theoremtpeq2d 3812 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)       (φ → {C, A, D} = {C, B, D})

Theoremtpeq3d 3813 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)       (φ → {C, D, A} = {C, D, B})

Theoremtpeq123d 3814 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)    &   (φC = D)    &   (φE = F)       (φ → {A, C, E} = {B, D, F})

Theoremtprot 3815 Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
{A, B, C} = {B, C, A}

Theoremtpcoma 3816 Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
{A, B, C} = {B, A, C}

Theoremtpcomb 3817 Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
{A, B, C} = {A, C, B}

Theoremtpass 3818 Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
{A, B, C} = ({A} ∪ {B, C})

Theoremqdass 3819 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
({A, B} ∪ {C, D}) = ({A, B, C} ∪ {D})

Theoremqdassr 3820 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
({A, B} ∪ {C, D}) = ({A} ∪ {B, C, D})

Theoremtpidm12 3821 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}

Theoremtpidm13 3822 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}

Theoremtpidm23 3823 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}

Theoremtpidm 3824 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}

Theoremprid1g 3825 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
(A VA {A, B})

Theoremprid2g 3826 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
(B VB {A, B})

Theoremprid1 3827 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}

Theoremprid2 3828 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}

Theoremtpid1 3829 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}

Theoremtpid2 3830 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}

Theoremtpid3g 3831 Closed theorem form of tpid3 3832. 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 BA {C, D, A})

Theoremtpid3 3832 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}

Theoremsnnzg 3833 The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
(A V → {A} ≠ )

Theoremsnnz 3834 The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
A V       {A} ≠

Theoremprnz 3835 A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
A V       {A, B} ≠

Theoremprnzg 3836 A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
(A V → {A, B} ≠ )

Theoremtpnz 3837 A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
A V       {A, B, C} ≠

Theoremsnss 3838 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)

Theoremeldifsn 3839 Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
(A (B {C}) ↔ (A B AC))

Theoremeldifsni 3840 Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
(A (B {C}) → AC)

Theoremneldifsn 3841 A is not in (B {A}). (Contributed by David Moews, 1-May-2017.)
¬ A (B {A})

Theoremneldifsnd 3842 A is not in (B {A}). Deduction form. (Contributed by David Moews, 1-May-2017.)
(φ → ¬ A (B {A}))

Theoremrexdifsn 3843 Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
(x (A {B})φx A (xB φ))

Theoremsnssg 3844 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))

Theoremdifsn 3845 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)

Theoremdifprsnss 3846 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}

Theoremdifprsn1 3847 Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
(AB → ({A, B} {A}) = {B})

Theoremdifprsn2 3848 Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
(AB → ({A, B} {B}) = {A})

Theoremdiftpsn3 3849 Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
((AC BC) → ({A, B, C} {C}) = {A, B})

Theoremdifsnb 3850 (B {A}) equals B if and only if A is not a member of B. Generalization of difsn 3845. (Contributed by David Moews, 1-May-2017.)
A B ↔ (B {A}) = B)

Theoremdifsnpss 3851 (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)

Theoremsnssi 3852 The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
(A B → {A} B)

Theoremsnssd 3853 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)

Theoremdifsnid 3854 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)

Theorempwpw0 3855 Compute the power set of the power set of the empty set. (See pw0 4160 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 3881, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.)
{} = {, {}}

Theoremsnsspr1 3856 A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
{A} {A, B}

Theoremsnsspr2 3857 A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
{B} {A, B}

Theoremsnsstp1 3858 A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
{A} {A, B, C}

Theoremsnsstp2 3859 A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
{B} {A, B, C}

Theoremsnsstp3 3860 A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
{C} {A, B, C}

Theoremprss 3861 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)

Theoremprssg 3862 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))

Theoremprssi 3863 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)

Theoremsssn 3864 The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
(A {B} ↔ (A = A = {B}))

Theoremssunsn2 3865 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 3884. (Contributed by Mario Carneiro, 2-Jul-2016.)
((B A A (C ∪ {D})) ↔ ((B A A C) ((B ∪ {D}) A A (C ∪ {D}))))

Theoremssunsn 3866 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})))

Theoremeqsn 3867* Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.)
(A → (A = {B} ↔ x A x = B))

Theoremssunpr 3868 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}))))

Theoremsspr 3869 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})))

Theoremsstp 3870 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}))))

Theoremtpss 3871 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)

Theoremsneqr 3872 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)

Theoremsnsssn 3873 If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
A V       ({A} {B} → A = B)

Theoremsneqrg 3874 Closed form of sneqr 3872. (Contributed by Scott Fenton, 1-Apr-2011.)
(A V → ({A} = {B} → A = B))

Theoremsneqbg 3875 Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
(A V → ({A} = {B} ↔ A = B))

Theoremsneqb 3876 Biconditional equality for singletons. (Contributed by SF, 14-Jan-2015.)
A V       ({A} = {B} ↔ A = B)

Theoremsnsspw 3877 The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)
{A} A

Theoremprsspw 3878 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))

Theoremralunsn 3879* 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 φ ψ)))

Theorem2ralunsn 3880* 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 χ θ))))

Theorempwsn 3881 The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
{A} = {, {A}}

TheorempwsnALT 3882 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}}

Theorempwpr 3883 The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
{A, B} = ({, {A}} ∪ {{B}, {A, B}})

Theorempwtp 3884 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}}))

Theorempwpwpw0 3885 Compute the power set of the power set of the power set of the empty set. (See also pw0 4160 and pwpw0 3855.) (Contributed by NM, 2-May-2009.)
{, {}} = ({, {}} ∪ {{{}}, {, {}}})

Theorempwv 3886 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

Theoremunsneqsn 3887 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}))

Theoremdfpss4 3888* Alternate definition of proper subset. Theorem IX.4.21 of [Rosser] p. 236. (Contributed by SF, 19-Jan-2015.)
(AB ↔ (A B x B ¬ x A))

Theoremadj11 3889 Adjoining a new element is one-to-one. (Contributed by SF, 29-Jan-2015.)
((¬ C A ¬ C B) → ((A ∪ {C}) = (B ∪ {C}) ↔ A = B))

Theoremdisj5 3890 Two ways of saying that two classes are disjoint. (Contributed by SF, 5-Feb-2015.)
((AB) = A B)

2.1.17  The union of a class

Syntaxcuni 3891 Extend class notation to include the union of a class (read: 'union A')
class A

Definitiondf-uni 3892* 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 3214. (Contributed by NM, 23-Aug-1993.)
A = {x y(x y y A)}

Theoremdfuni2 3893* Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
A = {x y A x y}

Theoremeluni 3894* Membership in class union. (Contributed by NM, 22-May-1994.)
(A Bx(A x x B))

Theoremeluni2 3895* Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
(A Bx B A x)

Theoremelunii 3896 Membership in class union. (Contributed by NM, 24-Mar-1995.)
((A B B C) → A C)

Theoremnfuni 3897 Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
xA       xA

Theoremnfunid 3898 Deduction version of nfuni 3897. (Contributed by NM, 18-Feb-2013.)
(φxA)       (φxA)

Theoremcsbunig 3899 Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
(A V[A / x]B = [A / x]B)

Theoremunieq 3900 Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(A = BA = B)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >