HomeHome Intuitionistic Logic Explorer
Theorem List (p. 36 of 95)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 3501-3600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdifsnss 3501 If we remove a single element from a class then put it back in, we end up with a subset of the original class. In classical logic, we could replace subset with equality. (Contributed by Jim Kingdon, 10-Aug-2018.)
 \  { }  u.  { }  C_
 
Theorempw0 3502 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 (/)  { (/) }
 
Theoremsnsspr1 3503 A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)

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

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

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

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

 { C }  C_  { ,  ,  C }
 
Theoremprsstp12 3508 A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)

 { ,  }  C_  { ,  ,  C }
 
Theoremprsstp13 3509 A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)

 { ,  C }  C_  { ,  ,  C }
 
Theoremprsstp23 3510 A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)

 { ,  C }  C_  { ,  ,  C }
 
Theoremprss 3511 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.)
 _V   &     _V   =>     C  C  { ,  }  C_  C
 
Theoremprssg 3512 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.)
 V  W  C  C  { ,  }  C_  C
 
Theoremprssi 3513 A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
 C  C  { ,  }  C_  C
 
Theoremprsspwg 3514 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.)
 V  W  { ,  }  C_  ~P C  C_  C  C_  C
 
Theoremsssnr 3515 Empty set and the singleton itself are subsets of a singleton. (Contributed by Jim Kingdon, 10-Aug-2018.)
 (/)  { }  C_  { }
 
Theoremsssnm 3516* The inhabited subset of a singleton. (Contributed by Jim Kingdon, 10-Aug-2018.)
 C_  { }  { }
 
Theoremeqsnm 3517* Two ways to express that an inhabited set equals a singleton. (Contributed by Jim Kingdon, 11-Aug-2018.)
 { }
 
Theoremssprr 3518 The subsets of a pair. (Contributed by Jim Kingdon, 11-Aug-2018.)
 (/)  { }  { C }  { ,  C }  C_  { ,  C }
 
Theoremsstpr 3519 The subsets of a triple. (Contributed by Jim Kingdon, 11-Aug-2018.)
 (/)  { }  { C }  { ,  C }  { D }  { ,  D }  { C ,  D }  { ,  C ,  D }  C_ 
 { ,  C ,  D }
 
Theoremtpss 3520 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.)
 _V   &     _V   &     C  _V   =>     D  D  C  D  { ,  ,  C }  C_  D
 
Theoremtpssi 3521 A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
 D  D  C  D  { ,  ,  C }  C_  D
 
Theoremsneqr 3522 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.)
 _V   =>     { }  { }
 
Theoremsnsssn 3523 If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
 _V   =>     { }  C_ 
 { }
 
Theoremsneqrg 3524 Closed form of sneqr 3522. (Contributed by Scott Fenton, 1-Apr-2011.)
 V  { }  { }
 
Theoremsneqbg 3525 Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
 V  { }  { }
 
Theoremsnsspw 3526 The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)

 { }  C_  ~P
 
Theoremprsspw 3527 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.)
 _V   &     _V   =>     { ,  }  C_  ~P C  C_  C  C_  C
 
Theorempreqr1g 3528 Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 3530. (Contributed by Jim Kingdon, 21-Sep-2018.)
 _V  _V  { ,  C }  { ,  C }
 
Theorempreqr2g 3529 Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the second elements are equal. Closed form of preqr2 3531. (Contributed by Jim Kingdon, 21-Sep-2018.)
 _V  _V  { C ,  }  { C ,  }
 
Theorempreqr1 3530 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.)
 _V   &     _V   =>     { ,  C }  { ,  C }
 
Theorempreqr2 3531 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.)
 _V   &     _V   =>     { C ,  }  { C ,  }
 
Theorempreq12b 3532 Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
 _V   &     _V   &     C  _V   &     D  _V   =>     { ,  }  { C ,  D }  C  D  D  C
 
Theoremprel12 3533 Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)
 _V   &     _V   &     C  _V   &     D  _V   =>     { ,  }  { C ,  D }  { C ,  D }  { C ,  D }
 
Theoremopthpr 3534 A way to represent ordered pairs using unordered pairs with distinct members. (Contributed by NM, 27-Mar-2007.)
 _V   &     _V   &     C  _V   &     D  _V   =>     =/=  D  { ,  }  { C ,  D }  C  D
 
Theorempreq12bg 3535 Closed form of preq12b 3532. (Contributed by Scott Fenton, 28-Mar-2014.)
 V  W  C  X  D  Y  { ,  }  { C ,  D }  C  D  D  C
 
Theoremprneimg 3536 Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 U  V  C  X  D  Y  =/=  C  =/=  D  =/=  C  =/=  D  { ,  }  =/=  { C ,  D }
 
Theorempreqsn 3537 Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
 _V   &     _V   &     C  _V   =>     { ,  }  { C }  C
 
Theoremdfopg 3538 Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
 V  W  <. ,  >.  { { } ,  { ,  } }
 
Theoremdfop 3539 Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.)
 _V   &     _V   =>     <. ,  >.  { { } ,  { ,  } }
 
Theoremopeq1 3540 Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
 <. ,  C >.  <. ,  C >.
 
Theoremopeq2 3541 Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
 <. C ,  >.  <. C ,  >.
 
Theoremopeq12 3542 Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
 C  D  <. ,  >.  <. C ,  D >.
 
Theoremopeq1i 3543 Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
   =>    
 <. ,  C >. 
 <. ,  C >.
 
Theoremopeq2i 3544 Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
   =>    
 <. C ,  >. 
 <. C ,  >.
 
Theoremopeq12i 3545 Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
   &     C  D   =>     <. ,  C >.  <. ,  D >.
 
Theoremopeq1d 3546 Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
   =>     <. ,  C >.  <. ,  C >.
 
Theoremopeq2d 3547 Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
   =>     <. C ,  >.  <. C ,  >.
 
Theoremopeq12d 3548 Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
   &     C  D   =>     <. ,  C >.  <. ,  D >.
 
Theoremoteq1 3549 Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
 <. ,  C ,  D >.  <. ,  C ,  D >.
 
Theoremoteq2 3550 Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
 <. C ,  ,  D >.  <. C ,  ,  D >.
 
Theoremoteq3 3551 Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
 <. C ,  D ,  >.  <. C ,  D ,  >.
 
Theoremoteq1d 3552 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
   =>     <. ,  C ,  D >.  <. ,  C ,  D >.
 
Theoremoteq2d 3553 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
   =>     <. C ,  ,  D >.  <. C ,  ,  D >.
 
Theoremoteq3d 3554 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
   =>     <. C ,  D ,  >.  <. C ,  D ,  >.
 
Theoremoteq123d 3555 Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
   &     C  D   &     E  F   =>     <. ,  C ,  E >.  <. ,  D ,  F >.
 
Theoremnfop 3556 Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
 F/_   &     F/_   =>     F/_ <. ,  >.
 
Theoremnfopd 3557 Deduction version of bound-variable hypothesis builder nfop 3556. This shows how the deduction version of a not-free theorem such as nfop 3556 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.)
 F/_   &     F/_   =>     F/_ <. ,  >.
 
Theoremopid 3558 The ordered pair  <. ,  >. in Kuratowski's representation. (Contributed by FL, 28-Dec-2011.)
 _V   =>    
 <. ,  >. 
 { { } }
 
Theoremralunsn 3559* 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.)
   =>     C  u.  { }
 
Theorem2ralunsn 3560* Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
   &       &       =>     C  u.  { }  u.  { }
 
Theoremopprc 3561 Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
 _V  _V  <. ,  >.  (/)
 
Theoremopprc1 3562 Expansion of an ordered pair when the first member is a proper class. See also opprc 3561. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
 _V  <. ,  >.  (/)
 
Theoremopprc2 3563 Expansion of an ordered pair when the second member is a proper class. See also opprc 3561. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
 _V  <. ,  >.  (/)
 
Theoremoprcl 3564 If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
 C  <. ,  >.  _V  _V
 
Theorempwsnss 3565 The power set of a singleton. (Contributed by Jim Kingdon, 12-Aug-2018.)

 { (/) ,  { } }  C_  ~P { }
 
Theorempwpw0ss 3566 Compute the power set of the power set of the empty set. (See pw0 3502 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48 (but with subset in place of equality). (Contributed by Jim Kingdon, 12-Aug-2018.)

 { (/) ,  { (/) } }  C_ 
 ~P { (/) }
 
Theorempwprss 3567 The power set of an unordered pair. (Contributed by Jim Kingdon, 13-Aug-2018.)
 { (/) ,  { } }  u.  { { } ,  { ,  } }  C_  ~P { ,  }
 
Theorempwtpss 3568 The power set of an unordered triple. (Contributed by Jim Kingdon, 13-Aug-2018.)
 { (/) ,  { } }  u.  { { } ,  { ,  } }  u.  { { C } ,  { ,  C } }  u.  { { ,  C } ,  { ,  ,  C } }  C_  ~P { ,  ,  C }
 
Theorempwpwpw0ss 3569 Compute the power set of the power set of the power set of the empty set. (See also pw0 3502 and pwpw0ss 3566.) (Contributed by Jim Kingdon, 13-Aug-2018.)
 { (/) ,  { (/)
 } }  u.  { { { (/) } } ,  { (/) ,  { (/) } } }  C_  ~P { (/)
 ,  { (/) } }
 
Theorempwv 3570 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
 
2.1.18  The union of a class
 
Syntaxcuni 3571 Extend class notation to include the union of a class (read: 'union ')
 U.
 
Definitiondf-uni 3572* 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 } . This is similar to the union of two classes df-un 2916. (Contributed by NM, 23-Aug-1993.)

 U.  {  |  }
 
Theoremdfuni2 3573* Alternate definition of class union. (Contributed by NM, 28-Jun-1998.)

 U.  {  |  }
 
Theoremeluni 3574* Membership in class union. (Contributed by NM, 22-May-1994.)
 U.
 
Theoremeluni2 3575* Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
 U.
 
Theoremelunii 3576 Membership in class union. (Contributed by NM, 24-Mar-1995.)
 C  U. C
 
Theoremnfuni 3577 Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 F/_   =>     F/_ U.
 
Theoremnfunid 3578 Deduction version of nfuni 3577. (Contributed by NM, 18-Feb-2013.)
 F/_   =>     F/_ U.
 
Theoremcsbunig 3579 Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.)
 V  [_  ]_
 U.  U. [_  ]_
 
Theoremunieq 3580 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.)
 U.  U.
 
Theoremunieqi 3581 Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.)
   =>    
 U.  U.
 
Theoremunieqd 3582 Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
   =>     U.  U.
 
Theoremeluniab 3583* Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
 U. {  |  }
 
Theoremelunirab 3584* Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.)
 U. {  | 
 }
 
Theoremunipr 3585 The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.)
 _V   &     _V   =>     U. { ,  }  u.
 
Theoremuniprg 3586 The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.)
 V  W  U. { ,  }  u.
 
Theoremunisn 3587 A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
 _V   =>    
 U. { }
 
Theoremunisng 3588 A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
 V  U. { }
 
Theoremdfnfc2 3589* An alternative statement of the effective freeness of a class , when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.)
 V  F/_  F/
 
Theoremuniun 3590 The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)

 U.  u.  U.  u.  U.
 
Theoremuniin 3591 The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

 U.  i^i  C_  U.  i^i  U.
 
Theoremuniss 3592 Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
 C_  U.  C_  U.
 
Theoremssuni 3593 Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
 C_  C  C_  U. C
 
Theoremunissi 3594 Subclass relationship for subclass union. Inference form of uniss 3592. (Contributed by David Moews, 1-May-2017.)
 C_    =>    
 U.  C_  U.
 
Theoremunissd 3595 Subclass relationship for subclass union. Deduction form of uniss 3592. (Contributed by David Moews, 1-May-2017.)
 C_    =>     U.  C_  U.
 
Theoremuni0b 3596 The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.)
 U.  (/)  C_  { (/) }
 
Theoremuni0c 3597* The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.)
 U.  (/)  (/)
 
Theoremuni0 3598 The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)

 U. (/)  (/)
 
Theoremelssuni 3599 An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
 C_  U.
 
Theoremunissel 3600 Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006.)
 U.  C_  U.
    < 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-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9427
  Copyright terms: Public domain < Previous  Next >