HomeHome New Foundations Explorer
Theorem List (p. 39 of 64)
< Previous  Next >
Browser slow? Try the
Unicode 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.)
 
Theorempreq1i 3802 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>   
 
Theorempreq2i 3803 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>   
 
Theorempreq12i 3804 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   &       =>   
 
Theorempreq1d 3805 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>   
 
Theorempreq2d 3806 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>   
 
Theorempreq12d 3807 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   &       =>   
 
Theoremtpeq1 3808 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
 
Theoremtpeq2 3809 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
 
Theoremtpeq3 3810 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
 
Theoremtpeq1d 3811 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   =>   
 
Theoremtpeq2d 3812 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   =>   
 
Theoremtpeq3d 3813 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   =>   
 
Theoremtpeq123d 3814 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   &       &       =>   
 
Theoremtprot 3815 Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
 
Theoremtpcoma 3816 Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
 
Theoremtpcomb 3817 Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
 
Theoremtpass 3818 Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
 
Theoremqdass 3819 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
 
Theoremqdassr 3820 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
 
Theoremtpidm12 3821 Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.)
 
Theoremtpidm13 3822 Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.)
 
Theoremtpidm23 3823 Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.)
 
Theoremtpidm 3824 Unordered triple is just an overlong way to write . (Contributed by David A. Wheeler, 10-May-2015.)
 
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.)
 
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.)
 
Theoremprid1 3827 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremprid2 3828 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
   =>   
 
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.)
   =>   
 
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.)
   =>   
 
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.)
 
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.)
   =>   
 
Theoremsnnzg 3833 The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
 
Theoremsnnz 3834 The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
   =>   
 
Theoremprnz 3835 A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
   =>   
 
Theoremprnzg 3836 A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
 
Theoremtpnz 3837 A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
   =>   
 
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.)
   =>   
 
Theoremeldifsn 3839 Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
 
Theoremeldifsni 3840 Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
 
Theoremneldifsn 3841 is not in . (Contributed by David Moews, 1-May-2017.)
 
Theoremneldifsnd 3842 is not in . Deduction form. (Contributed by David Moews, 1-May-2017.)
 
Theoremrexdifsn 3843 Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
 
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.)
 
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.)
 
Theoremdifprsnss 3846 Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
 
Theoremdifprsn1 3847 Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
 
Theoremdifprsn2 3848 Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 
Theoremdiftpsn3 3849 Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 
Theoremdifsnb 3850 equals if and only if is not a member of . Generalization of difsn 3845. (Contributed by David Moews, 1-May-2017.)
 
Theoremdifsnpss 3851 is a proper subclass of if and only if is a member of . (Contributed by David Moews, 1-May-2017.)
 
Theoremsnssi 3852 The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
 
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.)
   =>   
 
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.)
 
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.)
 
Theoremsnsspr2 3857 A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
 
Theoremsnsstp1 3858 A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
 
Theoremsnsstp2 3859 A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
 
Theoremsnsstp3 3860 A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
 
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.)
   &       =>   
 
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.)
 
Theoremprssi 3863 A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
 
Theoremsssn 3864 The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
 
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.)
 
Theoremssunsn 3866 Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
 
Theoremeqsn 3867* Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.)
 
Theoremssunpr 3868 Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
 
Theoremsspr 3869 The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.)
 
Theoremsstp 3870 The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
 
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.)
   &       &       =>   
 
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.)
   =>   
 
Theoremsnsssn 3873 If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
   =>   
 
Theoremsneqrg 3874 Closed form of sneqr 3872. (Contributed by Scott Fenton, 1-Apr-2011.)
 
Theoremsneqbg 3875 Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
 
Theoremsneqb 3876 Biconditional equality for singletons. (Contributed by SF, 14-Jan-2015.)
   =>   
 
Theoremsnsspw 3877 The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)
 
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.)
   &       =>   
 
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.)
   =>   
 
Theorem2ralunsn 3880* Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
   &       &       =>   
 
Theorempwsn 3881 The power set of a singleton. (Contributed by NM, 5-Jun-2006.)
 
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.)
 
Theorempwpr 3883 The power set of an unordered pair. (Contributed by NM, 1-May-2009.)
 
Theorempwtp 3884 The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
 
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.)
 
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.)
   =>   
 
Theoremdfpss4 3888* Alternate definition of proper subset. Theorem IX.4.21 of [Rosser] p. 236. (Contributed by SF, 19-Jan-2015.)
 
Theoremadj11 3889 Adjoining a new element is one-to-one. (Contributed by SF, 29-Jan-2015.)
 
Theoremdisj5 3890 Two ways of saying that two classes are disjoint. (Contributed by SF, 5-Feb-2015.)
 
2.1.17  The union of a class
 
Syntaxcuni 3891 Extend class notation to include the union of a class (read: 'union ')
 
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.)
 
Theoremdfuni2 3893* Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)
 
Theoremeluni 3894* Membership in class union. (Contributed by NM, 22-May-1994.)
 
Theoremeluni2 3895* Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
 
Theoremelunii 3896 Membership in class union. (Contributed by NM, 24-Mar-1995.)
 
Theoremnfuni 3897 Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 F/_   =>     F/_
 
Theoremnfunid 3898 Deduction version of nfuni 3897. (Contributed by NM, 18-Feb-2013.)
 F/_   =>     F/_
 
Theoremcsbunig 3899 Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
 
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.)
    < Previous  Next >

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-6338
  Copyright terms: Public domain < Previous  Next >