Home Higher-Order Logic ExplorerTheorem List (p. 2 of 3) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  HOLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Higher-Order Logic Explorer - 101-200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremoveq2 101 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremoveq 102 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-hbl1 103 is bound in . (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremhbl1 104 Inference form of ax-hbl1 103. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-17 105* If does not appear in , then any substitution to yields again, i.e. is a constant function. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theorema17i 106* Inference form of ax-17 105. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremhbxfrf 107* Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremhbxfr 108* Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremhbth 109* Hypothesis builder for a theorem. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremhbc 110 Hypothesis builder for combination. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremhbov 111 Hypothesis builder for binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremhbl 112* Hypothesis builder for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-inst 113* Instantiate a theorem with a new term. The second and third hypotheses are the HOL equivalent of set.mm "effectively not free in" predicate (see set.mm's ax-17, or ax17m 218). (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoreminsti 114* Instantiate a theorem with a new term. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremclf 115* Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremcl 116* Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremovl 117* Evaluate a lambda expression in a binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)

term

Syntaxtan 119 Conjunction term.
term

Syntaxtne 120 Negation term.
term

Syntaxtim 121 Implication term.
term

Syntaxtal 122 For all term.
term

Syntaxtex 123 There exists term.
term

Syntaxtor 124 Disjunction term.
term

Syntaxteu 125 There exists unique term.
term

Definitiondf-al 126* Define the for all operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-fal 127 Define the constant false. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-an 128* Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-im 129* Define the implication operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-not 130 Define the negation operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-ex 131* Define the existence operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-or 132* Define the 'or' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-eu 133* Define the 'exists unique' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwal 134 For all type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwfal 135 Contradiction type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwan 136 Conjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwim 137 Implication type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwnot 138 Negation type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwex 139 There exists type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwor 140 Disjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremweu 141 There exists unique type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremalval 142* Value of the for all predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremexval 143* Value of the 'there exists' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremeuval 144* Value of the 'exists unique' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremnotval 145 Value of negation. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremimval 146 Value of the implication. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremorval 147* Value of the disjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremanval 148* Value of the conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremax4g 149 If is true for all , then it is true for . (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremax4 150 If is true for all , then it is true for . (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremalrimiv 151* If one can prove where does not contain , then is true for all . (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremcla4v 152* If is true for all , then it is true for . (Contributed by Mario Carneiro, 9-Oct-2014.)

Theorempm2.21 153 A falsehood implies anything. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremdfan2 154 An alternative definition of the "and" term in terms of the context conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremhbct 155 Hypothesis builder for context conjunction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremmpd 156 Modus ponens. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremimp 157 Importation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremex 158 Exportation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremnotval2 159 Another way two write , the negation of . (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremnotnot1 160 One side of notnot 200. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremcon2d 161 A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremcon3d 162 A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremecase 163 Elimination by cases. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremolc 164 Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremorc 165 Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremexlimdv2 166* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremexlimdv 167* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremax4e 168 Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremcla4ev 169* Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theorem19.8a 170 Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)

0.3  Type definition mechanism

SyntaxwffMMJ2d 171 Internal axiom for mmj2 use.
wff typedef

Axiomax-wabs 172 Type of the abstraction function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
typedef

Axiomax-wrep 173 Type of the representation function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
typedef

Theoremwabs 174 Type of the abstraction function. (Contributed by Mario Carneiro, 8-Oct-2014.)
typedef

Theoremwrep 175 Type of the representation function. (Contributed by Mario Carneiro, 8-Oct-2014.)
typedef

Axiomax-tdef 176* The type definition axiom. The last hypothesis corresponds to the actual definition one wants to make; here we are defining a new type and the definition will provide us with pair of bijections mapping the new type to the subset of the old type such that is true. In order for this to be a valid (conservative) extension, we must ensure that the new type is nonempty, and for that purpose we need a witness that is not always false. (Contributed by Mario Carneiro, 8-Oct-2014.)
typedef

0.4  Extensionality

Axiomax-eta 177* The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremeta 178* The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremcbvf 179* Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremcbv 180* Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremleqf 181* Equality theorem for lambda abstraction, using bound variable instead of distinct variables. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremalrimi 182* If one can prove where does not contain , then is true for all . (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremexlimd 183* Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremalimdv 184* Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremeximdv 185* Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremalnex 186* Theorem 19.7 of [Margaris] p. 89. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremexnal1 187* Forward direction of exnal 201. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremisfree 188* Derive the metamath "is free" predicate in terms of the HOL "is free" predicate. (Contributed by Mario Carneiro, 9-Oct-2014.)

0.5  Axioms of infinity and choice

Syntaxtf11 189 One-to-one function.
term 1-1

Syntaxtfo 190 Onto function.
term onto

Syntaxtat 191 Indefinite descriptor.
term

Axiomax-wat 192 The type of the indefinite descriptor. (New usage is discouraged.) (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremwat 193 The type of the indefinite descriptor. (Contributed by Mario Carneiro, 10-Oct-2014.)

Definitiondf-f11 194* Define a one-to-one function. (Contributed by Mario Carneiro, 10-Oct-2014.)
1-1

Definitiondf-fo 195* Define an onto function. (Contributed by Mario Carneiro, 10-Oct-2014.)
onto

Axiomax-ac 196* Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremac 197 Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremdfex2 198 Alternative definition of the "there exists" quantifier. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremexmid 199 Diaconescu's theorem, which derives the law of the excluded middle from the axiom of choice. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremnotnot 200 Rule of double negation. (Contributed by Mario Carneiro, 10-Oct-2014.)

Page List