HomeHome Intuitionistic Logic Explorer
Theorem List (p. 45 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 - 4401-4500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremreliun 4401 An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)
 Rel  U_  Rel
 
Theoremreliin 4402 An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
 Rel  Rel  |^|_
 
Theoremreluni 4403* The union of a class is a relation iff any member is a relation. Exercise 6 of [TakeutiZaring] p. 25 and its converse. (Contributed by NM, 13-Aug-2004.)
 Rel  U.  Rel
 
Theoremrelint 4404* The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014.)
 Rel  Rel  |^|
 
Theoremrel0 4405 The empty set is a relation. (Contributed by NM, 26-Apr-1998.)

 Rel  (/)
 
Theoremrelopabi 4406 A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
 { <. ,  >.  |  }   =>     Rel
 
Theoremrelopab 4407 A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) (Unnecessary distinct variable restrictions were removed by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)

 Rel  { <. ,  >.  |  }
 
Theoremreli 4408 The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)

 Rel  _I
 
Theoremrele 4409 The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)

 Rel  _E
 
Theoremopabid2 4410* A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.)
 Rel  {
 <. ,  >.  | 
 <. ,  >.  }
 
Theoreminopab 4411* Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
 { <. ,  >.  |  }  i^i  {
 <. ,  >.  |  }  { <. ,  >.  |  }
 
Theoremdifopab 4412* The difference of two ordered-pair abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
 { <. ,  >.  |  }  \  { <. ,  >.  |  }  { <. ,  >.  |  }
 
Theoreminxp 4413 The intersection of two cross products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 X.  i^i  C  X.  D 
 i^i  C  X.  i^i  D
 
Theoremxpindi 4414 Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
 X.  i^i  C 
 X.  i^i  X.  C
 
Theoremxpindir 4415 Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
 i^i  X.  C 
 X.  C  i^i  X.  C
 
Theoremxpiindim 4416* Distributive law for cross product over indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
 C  X.  |^|_  |^|_  C  X.
 
Theoremxpriindim 4417* Distributive law for cross product over relativized indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
 C  X.  D  i^i  |^|_  C  X.  D 
 i^i  |^|_  C  X.
 
Theoremeliunxp 4418* Membership in a union of cross products. Analogue of elxp 4305 for nonconstant . (Contributed by Mario Carneiro, 29-Dec-2014.)
 C  U_  { }  X.  C  <. ,  >.
 
Theoremopeliunxp2 4419* Membership in a union of cross products. (Contributed by Mario Carneiro, 14-Feb-2015.)
 C  E   =>     <. C ,  D >.  U_  { }  X.  C  D  E
 
Theoremraliunxp 4420* Write a double restricted quantification as one universal quantifier. In this version of ralxp 4422, is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
 <. ,  >.    =>     U_  { }  X.
 
Theoremrexiunxp 4421* Write a double restricted quantification as one universal quantifier. In this version of rexxp 4423, is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
 <. ,  >.    =>     U_  { }  X.
 
Theoremralxp 4422* Universal quantification restricted to a cross product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)
 <. ,  >.    =>     X.
 
Theoremrexxp 4423* Existential quantification restricted to a cross product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.)
 <. ,  >.    =>     X.
 
Theoremdjussxp 4424* Disjoint union is a subset of a cross product. (Contributed by Stefan O'Rear, 21-Nov-2014.)
 U_  { }  X.  C_ 
 X.  _V
 
Theoremralxpf 4425* Version of ralxp 4422 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.)

 F/   &     F/   &     F/   &     <. ,  >.    =>     X.
 
Theoremrexxpf 4426* Version of rexxp 4423 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.)

 F/   &     F/   &     F/   &     <. ,  >.    =>     X.
 
Theoremiunxpf 4427* Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
 F/_ C   &     F/_ C   &     F/_ D   &     <. ,  >.  C  D   =>     U_  X.  C  U_  U_  D
 
Theoremopabbi2dv 4428* Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2153. (Contributed by NM, 24-Feb-2014.)

 Rel    &     <. ,  >.    =>     { <. ,  >.  |  }
 
Theoremrelop 4429* A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)
 _V   &     _V   =>     Rel  <. ,  >.  { }  { ,  }
 
Theoremideqg 4430 For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 V  _I
 
Theoremideq 4431 For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.)
 _V   =>     _I
 
Theoremididg 4432 A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 V  _I
 
Theoremissetid 4433 Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
 _V  _I
 
Theoremcoss1 4434 Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
 C_  o.  C  C_  o.  C
 
Theoremcoss2 4435 Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
 C_  C  o.  C_  C  o.
 
Theoremcoeq1 4436 Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
 o.  C  o.  C
 
Theoremcoeq2 4437 Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
 C  o.  C  o.
 
Theoremcoeq1i 4438 Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
   =>     o.  C  o.  C
 
Theoremcoeq2i 4439 Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
   =>     C  o.  C  o.
 
Theoremcoeq1d 4440 Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
   =>     o.  C  o.  C
 
Theoremcoeq2d 4441 Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
   =>     C  o.  C  o.
 
Theoremcoeq12i 4442 Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
   &     C  D   =>     o.  C  o.  D
 
Theoremcoeq12d 4443 Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
   &     C  D   =>     o.  C  o.  D
 
Theoremnfco 4444 Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
 F/_   &     F/_   =>     F/_  o.
 
Theorembrcog 4445* Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.)
 V  W  C  o.  D  D  C
 
Theoremopelco2g 4446* Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.)
 V  W  <. ,  >.  C  o.  D  <. ,  >.  D  <. ,  >.  C
 
Theorembrcogw 4447 Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.)
 V  W  X  Z  D X  X C  C  o.  D
 
Theoremeqbrrdva 4448* Deduction from extensionality principle for relations, given an equivalence only on the relation's domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.)
 C_  C  X.  D   &     C_  C  X.  D   &     C  D    =>   
 
Theorembrco 4449* Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.)
 _V   &     _V   =>     C  o.  D  D  C
 
Theoremopelco 4450* Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
 _V   &     _V   =>     <. ,  >.  C  o.  D  D  C
 
Theoremcnvss 4451 Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
 C_  `'  C_  `'
 
Theoremcnveq 4452 Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
 `'  `'
 
Theoremcnveqi 4453 Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
   =>     `'  `'
 
Theoremcnveqd 4454 Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
   =>     `'  `'
 
Theoremelcnv 4455* Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.)
 `' R  <. ,  >.  R
 
Theoremelcnv2 4456* Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.)
 `' R  <. ,  >.  <. ,  >.  R
 
Theoremnfcnv 4457 Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   =>     F/_ `'
 
Theoremopelcnvg 4458 Ordered-pair membership in converse. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 C  D  <. ,  >.  `' R  <. ,  >.  R
 
Theorembrcnvg 4459 The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.)
 C  D  `' R  R
 
Theoremopelcnv 4460 Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
 _V   &     _V   =>     <. ,  >.  `' R  <. ,  >.  R
 
Theorembrcnv 4461 The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.)
 _V   &     _V   =>     `' R  R
 
Theoremcsbcnvg 4462 Move class substitution in and out of the converse of a function. (Contributed by Thierry Arnoux, 8-Feb-2017.)
 V  `' [_  ]_ F  [_  ]_ `' F
 
Theoremcnvco 4463 Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 `'  o.  `'  o.  `'
 
Theoremcnvuni 4464* The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
 `' U.  U_  `'
 
Theoremdfdm3 4465* Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)

 dom  {  |  <. ,  >.  }
 
Theoremdfrn2 4466* Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.)

 ran  {  |  }
 
Theoremdfrn3 4467* Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.)

 ran  {  |  <. ,  >.  }
 
Theoremelrn2g 4468* Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
 V  ran  <. ,  >.
 
Theoremelrng 4469* Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.)
 V  ran
 
Theoremdfdm4 4470 Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)

 dom  ran  `'
 
Theoremdfdmf 4471* Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   &     F/_   =>     dom  {  |  }
 
Theoremcsbdmg 4472 Distribute proper substitution through the domain of a class. (Contributed by Jim Kingdon, 8-Dec-2018.)
 V  [_  ]_
 dom  dom  [_  ]_
 
Theoremeldmg 4473* Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.)
 V  dom
 
Theoremeldm2g 4474* Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.)
 V  dom  <. ,  >.
 
Theoremeldm 4475* Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.)
 _V   =>     dom
 
Theoremeldm2 4476* Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.)
 _V   =>     dom  <. ,  >.
 
Theoremdmss 4477 Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)
 C_  dom  C_  dom
 
Theoremdmeq 4478 Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)
 dom  dom
 
Theoremdmeqi 4479 Equality inference for domain. (Contributed by NM, 4-Mar-2004.)
   =>    
 dom  dom
 
Theoremdmeqd 4480 Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
   =>     dom  dom
 
Theoremopeldm 4481 Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995.)
 _V   &     _V   =>     <. ,  >.  C  dom  C
 
Theorembreldm 4482 Membership of first of a binary relation in a domain. (Contributed by NM, 30-Jul-1995.)
 _V   &     _V   =>     R  dom  R
 
Theoremopeldmg 4483 Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
 V  W  <. ,  >.  C  dom  C
 
Theorembreldmg 4484 Membership of first of a binary relation in a domain. (Contributed by NM, 21-Mar-2007.)
 C  D  R  dom  R
 
Theoremdmun 4485 The domain of a union is the union of domains. Exercise 56(a) of [Enderton] p. 65. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

 dom  u.  dom  u.  dom
 
Theoremdmin 4486 The domain of an intersection belong to the intersection of domains. Theorem 6 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.)

 dom  i^i  C_  dom 
 i^i  dom
 
Theoremdmiun 4487 The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016.)

 dom  U_  U_  dom
 
Theoremdmuni 4488* The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)

 dom  U.  U_  dom
 
Theoremdmopab 4489* The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 4-Dec-2016.)

 dom  { <. ,  >.  |  }  {  | 
 }
 
Theoremdmopabss 4490* Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)

 dom  { <. ,  >.  |  }  C_
 
Theoremdmopab3 4491* The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004.)
 dom  { <. ,  >.  |  }
 
Theoremdm0 4492 The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

 dom  (/)  (/)
 
Theoremdmi 4493 The domain of the identity relation is the universe. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

 dom  _I  _V
 
Theoremdmv 4494 The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003.)

 dom  _V  _V
 
Theoremdm0rn0 4495 An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)
 dom  (/)  ran  (/)
 
Theoremreldm0 4496 A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004.)
 Rel  (/)  dom  (/)
 
Theoremdmmrnm 4497* A domain is inhabited if and only if the range is inhabited. (Contributed by Jim Kingdon, 15-Dec-2018.)
 dom  ran
 
Theoremdmxpm 4498* The domain of a cross product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 dom  X.
 
Theoremdmxpinm 4499* The domain of the intersection of two square cross products. Unlike dmin 4486, equality holds. (Contributed by NM, 29-Jan-2008.)
 i^i  dom  X. 
 i^i  X.  i^i
 
Theoremxpid11m 4500* The cross product of a class with itself is one-to-one. (Contributed by Jim Kingdon, 8-Dec-2018.)

 X.  X.
    < 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 >