HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-11257) |
Hilbert Space Explorer
(11258-12844) |
Users' Mathboxes
(12845-19026) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bnj120 14001 | First-order logic and set theory. |
        
 
 
    pred        ![]](rbrack.gif){kind=small} 
pred | ||
| Theorem | bnj121 14002 | First-order logic and set theory. |
 FrSe  
  
FrSe
| ||
| Theorem | bnj122 14003 | First-order logic and set theory. |
  FrSe
FrSe
| ||
| Theorem | bnj123 14004 | Technical lemma of bnj150 14013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
    pred
  
 | ||
| Theorem | bnj124 14005 | Technical lemma of bnj150 14013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
FrSe
FrSe
| ||
| Theorem | bnj125 14006 | Technical lemma of bnj150 14013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred | ||
| Theorem | bnj126 14007 | Technical lemma of bnj150 14013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred
pred | ||
| Theorem | bnj127 14008 | Technical lemma of bnj150 14013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred FrSe
| ||
| Theorem | bnj128 14009 | Technical lemma of bnj150 14013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
| ||
| Theorem | bnj129 14010 | Technical lemma of bnj150 14013. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| FrSe
FrSe
FrSe
| ||
| Theorem | bnj130 14011 | Technical lemma of bnj151 14014. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
 FrSe
FrSe
| ||
| Theorem | bnj149 14012 | Technical lemma of bnj151 14014. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
 FrSe
      pred
| ||
| Theorem | bnj150 14013 | Technical lemma of bnj151 14014. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred
FrSe
 FrSe
pred
| ||
| Theorem | bnj151 14014 | Technical lemma of bnj152 14015. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred 
 FrSe
 
FrSe
FrSe
FrSe
pred
| ||
| Theorem | bnj152 14015 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
FrSe
FrSe
FrSe
pred
| ||
| Theorem | bnj154 14016 | Technical lemma of bnj153 14018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj155 14017 | Technical lemma of bnj153 14018. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred | ||
| Theorem | bnj153 14018 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
| ||
| Theorem | bnj207 14019 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
 FrSe
 FrSe | ||
| Theorem | bnj213 14020 | First-order logic and set theory. |
pred
 | ||
| Theorem | bnj218 14021 | Technical lemma of bnj515 14027. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred 
| ||
| Theorem | bnj222 14022 | Technical lemma of bnj229 14024. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred | ||
| Theorem | bnj223 14023 | Technical lemma of bnj229 14024. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred pred | ||
| Theorem | bnj229 14024 | Technical lemma of bnj513 14025. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
| ||
| Theorem | bnj513 14025 | Technical lemma of bnj154 14016. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
| ||
| Theorem | bnj514 14026 | Technical lemma of bnj515 14027. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
 | ||
| Theorem | bnj515 14027 | Technical lemma of bnj516 14028. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj516 14028 | Technical lemma of bnj212 14029. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj212 14029 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj517 14030 | Technical lemma of bnj518 14031. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj518 14031 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred
 FrSe
pred | ||
| Theorem | bnj522 14032 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred 
 pred
FrSe
| ||
| Theorem | bnj523 14033 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred | ||
| Theorem | bnj526 14034 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred | ||
| Theorem | bnj528 14035 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred | ||
| Theorem | bnj535 14036 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
FrSe
| ||
| Theorem | bnj539 14037 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred | ||
| Theorem | bnj540 14038 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred | ||
| Theorem | bnj541 14039 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
FrSe
 FrSe | ||
| Theorem | bnj543 14040 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred
pred 
FrSe
| ||
| Theorem | bnj544 14041 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
FrSe
| ||
| Theorem | bnj545 14042 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred pred
FrSe
pred FrSe
| ||
| Theorem | bnj546 14043 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred FrSe
pred | ||
| Theorem | bnj547 14044 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred
pred
pred
FrSe
| ||
| Theorem | bnj548 14045 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred 
pred
FrSe
FrSe
| ||
| Theorem | bnj549 14046 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj550 14047 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred 
pred
| ||
| Theorem | bnj552 14048 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj553 14049 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
pred
pred
pred
pred FrSe
FrSe
| ||
| Theorem | bnj554 14050 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred
pred
pred
| ||
| Theorem | bnj556 14051 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
| ||
| Theorem | bnj557 14052 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
pred
pred
pred
pred FrSe
FrSe
| ||
| Theorem | bnj558 14053 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
pred
pred
pred
pred FrSe
FrSe
| ||
| Theorem | bnj561 14054 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
FrSe FrSe
| ||
| Theorem | bnj562 14055 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
FrSe FrSe
| ||
| Theorem | bnj567 14056 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
FrSe
FrSe
| ||
| Theorem | bnj568 14057 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
FrSe
FrSe
| ||
| Theorem | bnj569 14058 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred FrSe
pred | ||
| Theorem | bnj570 14059 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
FrSe
pred FrSe
| ||
| Theorem | bnj571 14060 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
pred
pred
pred
pred FrSe
FrSe
pred FrSe
| ||
| Theorem | bnj573 14061 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj578 14062 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
FrSe
pred
pred
FrSe
FrSe
FrSe
FrSe
| ||
| Theorem | bnj605 14063 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
FrSe
pred
pred
FrSe
FrSe
FrSe
FrSe
| ||
| Theorem | bnj606 14064 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
FrSe
FrSe
FrSe FrSe
| ||
| Theorem | bnj581 14065 | Technical lemma of bnj580 14072. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 9-Jul-2011.) |
|
| ||
| Theorem | bnj582 14066 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| | ||
| Theorem | bnj583 14067 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred pred
pred
| ||
| Theorem | bnj589 14068 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
pred
pred | ||
| Theorem | bnj590 14069 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred | ||
| Theorem | bnj591 14070 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
 | ||
| Theorem | bnj594 14071 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
pred
| ||
| Theorem | bnj580 14072 | Technical lemma of bnj579 14073. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj579 14073 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
| ||
| Theorem | bnj602 14074 | Equality theorem for the pred function constant. |
 pred pred
| ||
| Theorem | bnj607 14075 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
FrSe
pred
pred
FrSe
FrSe
FrSe pred
pred   
FrSe
| ||
| Theorem | bnj608 14076 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
FrSe
pred
pred
FrSe
FrSe
FrSe pred
pred FrSe
| ||
| Theorem | bnj609 14077 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred | ||
| Theorem | bnj611 14078 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred | ||
| Theorem | bnj600 14079 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
pred
pred
pred
pred
pred
| ||
| Theorem | bnj601 14080 | Technical lemma of bnj75 14081. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
| ||
| Theorem | bnj75 14081 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
FrSe
| ||
| Theorem | bnj616 14082 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
| ||
| Theorem | bnj850 14083 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred FrSe
| ||
| Theorem | bnj852 14084 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
| ||
| Theorem | bnj854 14085 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| ||
| Theorem | bnj864 14086 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
| ||
| Theorem | bnj865 14087 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
| ||
| Theorem | bnj873 14088 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| ||
| Theorem | bnj849 14089 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
FrSe
FrSe
| ||
| Theorem | bnj881 14090 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
| ||
| Theorem | bnj882 14091 |
Definition (using hypotheses for readability) of the function giving the
transitive closure of in by .
|
pred
pred
trCl
 | ||
| Theorem | bnj891 14092 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred pred | ||
| Theorem | bnj892 14093 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
pred
pred | ||
| Theorem | bnj889 14094 | Technical lemma of bnj893 14095. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
pred
pred
FrSe
trCl | ||
| Theorem | bnj893 14095 |
Property of trCl. Under certain conditions, the transitive
closure of in
by is a set.
|
|
FrSe trCl
| ||
| Theorem | bnj900 14096 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
|
| ||
| Theorem | bnj902 14097 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred | ||
| Theorem | bnj894 14098 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
pred trCl | ||
| Theorem | bnj906 14099 | Property of trCl. |
|
FrSe pred
trCl | ||
| Theorem | bnj908 14100 | Technical lemma of bnj69 14226. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). |
| pred
pred
FrSe
pred
pred
pred
pred
pred
FrSe
| ||
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |