HomeHome Intuitionistic Logic Explorer
Theorem List (p. 35 of 94)
< 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 - 3401-3500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
TheoremrexsnsOLD 3401* Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) Obsolete as of 22-Aug-2018. Use rexsns 3400 instead. (New usage is discouraged.) (Proof modification is discouraged.)
 V  { }  [.  ].
 
Theoremralsng 3402* Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
   =>     V  { }
 
Theoremrexsng 3403* Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
   =>     V  { }
 
Theoremexsnrex 3404 There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018.)
 M  { }  M  M  { }
 
Theoremralsn 3405* Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
 _V   &       =>     { }
 
Theoremrexsn 3406* Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
 _V   &       =>     { }
 
Theoremeltpg 3407 Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
 V  { ,  C ,  D }  C  D
 
Theoremeltpi 3408 A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
 { ,  C ,  D }  C  D
 
Theoremeltp 3409 A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.)
 _V   =>     { ,  C ,  D }  C  D
 
Theoremdftp2 3410* Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.)

 { ,  ,  C }  {  |  C }
 
Theoremnfpr 3411 Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
 F/_   &     F/_   =>     F/_ { ,  }
 
Theoremralprg 3412* Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
   &       =>     V  W  { ,  }
 
Theoremrexprg 3413* Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
   &       =>     V  W  { ,  }
 
Theoremraltpg 3414* Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
   &       &     C    =>     V  W  C  X  { ,  ,  C }
 
Theoremrextpg 3415* Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
   &       &     C    =>     V  W  C  X  { ,  ,  C }
 
Theoremralpr 3416* Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
 _V   &     _V   &       &       =>     { ,  }
 
Theoremrexpr 3417* Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
 _V   &     _V   &       &       =>     { ,  }
 
Theoremraltp 3418* Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
 _V   &     _V   &     C  _V   &       &       &     C    =>     { ,  ,  C }
 
Theoremrextp 3419* Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
 _V   &     _V   &     C  _V   &       &       &     C    =>     { ,  ,  C }
 
Theoremsbcsng 3420* Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
 V  [.  ].  { }
 
Theoremnfsn 3421 Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
 F/_   =>     F/_ { }
 
Theoremcsbsng 3422 Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
 V  [_  ]_
 { }  {
 [_  ]_ }
 
Theoremdisjsn 3423 Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
 i^i  { }  (/)
 
Theoremdisjsn2 3424 Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
 =/=  { }  i^i  { }  (/)
 
Theoremdisjpr2 3425 The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
 =/=  C  =/=  C  =/=  D  =/=  D  { ,  }  i^i  { C ,  D }  (/)
 
Theoremsnprc 3426 The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 5-Aug-1993.)
 _V  { }  (/)
 
Theoremr19.12sn 3427* Special case of r19.12 2416 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.)
 _V   =>     { }  { }
 
Theoremrabsn 3428* Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
 {  |  }  { }
 
Theoremrabrsndc 3429* A class abstraction over a decidable proposition restricted to a singleton is either the empty set or the singleton itself. (Contributed by Jim Kingdon, 8-Aug-2018.)
 _V   &    DECID    =>     M  {  { }  | 
 }  M  (/)  M  { }
 
Theoremeuabsn2 3430* Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
 {  | 
 }  { }
 
Theoremeuabsn 3431 Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
 {  | 
 }  { }
 
Theoremreusn 3432* A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
 {  |  }  { }
 
Theoremabsneu 3433 Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
 V  {  | 
 }  { }
 
Theoremrabsneu 3434 Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
 V  {  |  }  { }
 
Theoremeusn 3435* Two ways to express " is a singleton." (Contributed by NM, 30-Oct-2010.)
 { }
 
Theoremrabsnt 3436* Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by NM, 29-May-2006.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
 _V   &       =>     {  |  }  { }
 
Theoremprcom 3437 Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)

 { ,  }  { ,  }
 
Theorempreq1 3438 Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
 { ,  C }  { ,  C }
 
Theorempreq2 3439 Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
 { C ,  }  { C ,  }
 
Theorempreq12 3440 Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
 C  D  { ,  }  { C ,  D }
 
Theorempreq1i 3441 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>    
 { ,  C }  { ,  C }
 
Theorempreq2i 3442 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>    
 { C ,  }  { C ,  }
 
Theorempreq12i 3443 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   &     C  D   =>     { ,  C }  { ,  D }
 
Theorempreq1d 3444 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>     { ,  C }  { ,  C }
 
Theorempreq2d 3445 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   =>     { C ,  }  { C ,  }
 
Theorempreq12d 3446 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
   &     C  D   =>     { ,  C }  { ,  D }
 
Theoremtpeq1 3447 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
 { ,  C ,  D }  { ,  C ,  D }
 
Theoremtpeq2 3448 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
 { C ,  ,  D }  { C ,  ,  D }
 
Theoremtpeq3 3449 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
 { C ,  D ,  }  { C ,  D ,  }
 
Theoremtpeq1d 3450 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   =>     { ,  C ,  D }  { ,  C ,  D }
 
Theoremtpeq2d 3451 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   =>     { C ,  ,  D }  { C ,  ,  D }
 
Theoremtpeq3d 3452 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   =>     { C ,  D ,  }  { C ,  D ,  }
 
Theoremtpeq123d 3453 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
   &     C  D   &     E  F   =>     { ,  C ,  E }  { ,  D ,  F }
 
Theoremtprot 3454 Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)

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

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

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

 { ,  ,  C }  { }  u.  { ,  C }
 
Theoremqdass 3458 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
 { ,  }  u.  { C ,  D }  { ,  ,  C }  u.  { D }
 
Theoremqdassr 3459 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
 { ,  }  u.  { C ,  D }  { }  u.  { ,  C ,  D }
 
Theoremtpidm12 3460 Unordered triple  { ,  ,  } is just an overlong way to write  { ,  }. (Contributed by David A. Wheeler, 10-May-2015.)

 { ,  ,  }  { ,  }
 
Theoremtpidm13 3461 Unordered triple  { ,  ,  } is just an overlong way to write  { ,  }. (Contributed by David A. Wheeler, 10-May-2015.)

 { ,  ,  }  { ,  }
 
Theoremtpidm23 3462 Unordered triple  { ,  ,  } is just an overlong way to write  { ,  }. (Contributed by David A. Wheeler, 10-May-2015.)

 { ,  ,  }  { ,  }
 
Theoremtpidm 3463 Unordered triple  { ,  ,  } is just an overlong way to write  { }. (Contributed by David A. Wheeler, 10-May-2015.)

 { ,  ,  }  { }
 
Theoremtppreq3 3464 An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 C  { ,  ,  C }  { ,  }
 
Theoremprid1g 3465 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
 V  { ,  }
 
Theoremprid2g 3466 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
 V  { ,  }
 
Theoremprid1 3467 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
 _V   =>     { ,  }
 
Theoremprid2 3468 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
 _V   =>     { ,  }
 
Theoremprprc1 3469 A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
 _V  { ,  }  { }
 
Theoremprprc2 3470 A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
 _V  { ,  }  { }
 
Theoremprprc 3471 An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
 _V  _V  { ,  }  (/)
 
Theoremtpid1 3472 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
 _V   =>     { ,  ,  C }
 
Theoremtpid2 3473 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
 _V   =>     { ,  ,  C }
 
Theoremtpid3g 3474 Closed theorem form of tpid3 3475. (Contributed by Alan Sare, 24-Oct-2011.)
 { C ,  D ,  }
 
Theoremtpid3 3475 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  { ,  ,  C }
 
Theoremsnnzg 3476 The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
 V  { }  =/=  (/)
 
Theoremsnmg 3477* The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
 V  { }
 
Theoremsnnz 3478 The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
 _V   =>    
 { }  =/=  (/)
 
Theoremsnm 3479* The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
 _V   =>     { }
 
Theoremprmg 3480* A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
 V  { ,  }
 
Theoremprnz 3481 A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
 _V   =>    
 { ,  }  =/=  (/)
 
Theoremprm 3482* A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
 _V   =>     { ,  }
 
Theoremprnzg 3483 A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
 V  { ,  }  =/=  (/)
 
Theoremtpnz 3484 A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
 _V   =>    
 { ,  ,  C }  =/=  (/)
 
Theoremsnss 3485 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.)
 _V   =>     { }  C_
 
Theoremeldifsn 3486 Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
 \  { C }  =/=  C
 
Theoremeldifsni 3487 Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
 \  { C }  =/=  C
 
Theoremneldifsn 3488 is not in 
\  { }. (Contributed by David Moews, 1-May-2017.)

 \  { }
 
Theoremneldifsnd 3489 is not in 
\  { }. Deduction form. (Contributed by David Moews, 1-May-2017.)
 \  { }
 
Theoremrexdifsn 3490 Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
 \  { }  =/=
 
Theoremsnssg 3491 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.)
 V  { }  C_
 
Theoremdifsn 3492 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 3493 Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
 { ,  }  \  { }  C_  { }
 
Theoremdifprsn1 3494 Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
 =/=  { ,  }  \  { }  { }
 
Theoremdifprsn2 3495 Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 =/=  { ,  }  \  { }  { }
 
Theoremdiftpsn3 3496 Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 =/=  C  =/=  C  { ,  ,  C }  \  { C }  { ,  }
 
Theoremdifsnb 3497  \  { } equals if and only if is not a member of . Generalization of difsn 3492. (Contributed by David Moews, 1-May-2017.)
 \  { }
 
Theoremdifsnpssim 3498  \  { } is a proper subclass of if is a member of . In classical logic, the converse holds as well. (Contributed by Jim Kingdon, 9-Aug-2018.)
 \  { }  C.
 
Theoremsnssi 3499 The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
 { }  C_
 
Theoremsnssd 3500 The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>     { }  C_
    < 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-9381
  Copyright terms: Public domain < Previous  Next >