P. 2 of Theorem List - Higher-Order Logic Explorer

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

Type	Label	Description
Statement
Theorem	oveq2 101	Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    &   ⊢ R⊧[B = T]    ⇒   ⊢ R⊧[[AFB] = [AFT]]
Theorem	oveq 102	Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    &   ⊢ R⊧[F = S]    ⇒   ⊢ R⊧[[AFB] = [ASB]]
Axiom	ax-hbl1 103	x is bound in λxA. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:γ    &   ⊢ B:α    ⇒   ⊢ ⊤⊧[(λx:α λx:β AB) = λx:β A]
Theorem	hbl1 104	Inference form of ax-hbl1 103. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:γ    &   ⊢ B:α    &   ⊢ R:∗    ⇒   ⊢ R⊧[(λx:α λx:β AB) = λx:β A]
Axiom	ax-17 105*	If x does not appear in A, then any substitution to A yields A again, i.e. λxA is a constant function. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ B:α    ⇒   ⊢ ⊤⊧[(λx:α AB) = A]
Theorem	a17i 106*	Inference form of ax-17 105. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ B:α    &   ⊢ R:∗    ⇒   ⊢ R⊧[(λx:α AB) = A]
Theorem	hbxfrf 107*	Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ T:β    &   ⊢ B:α    &   ⊢ R⊧[T = A]    &   ⊢ (S, R)⊧[(λx:α AB) = A]    ⇒   ⊢ (S, R)⊧[(λx:α TB) = T]
Theorem	hbxfr 108*	Transfer a hypothesis builder to an equivalent expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ T:β    &   ⊢ B:α    &   ⊢ R⊧[T = A]    &   ⊢ R⊧[(λx:α AB) = A]    ⇒   ⊢ R⊧[(λx:α TB) = T]
Theorem	hbth 109*	Hypothesis builder for a theorem. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ B:α    &   ⊢ R⊧A    ⇒   ⊢ R⊧[(λx:α AB) = A]
Theorem	hbc 110	Hypothesis builder for combination. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(β → γ)    &   ⊢ A:β    &   ⊢ B:α    &   ⊢ R⊧[(λx:α FB) = F]    &   ⊢ R⊧[(λx:α AB) = A]    ⇒   ⊢ R⊧[(λx:α (FA)B) = (FA)]
Theorem	hbov 111	Hypothesis builder for binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(β → (γ → δ))    &   ⊢ A:β    &   ⊢ B:α    &   ⊢ C:γ    &   ⊢ R⊧[(λx:α FB) = F]    &   ⊢ R⊧[(λx:α AB) = A]    &   ⊢ R⊧[(λx:α CB) = C]    ⇒   ⊢ R⊧[(λx:α [AFC]B) = [AFC]]
Theorem	hbl 112*	Hypothesis builder for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:γ    &   ⊢ B:α    &   ⊢ R⊧[(λx:α AB) = A]    ⇒   ⊢ R⊧[(λx:α λy:β AB) = λy:β A]
Axiom	ax-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.)
⊢ R⊧A    &   ⊢ ⊤⊧[(λx:α By:α) = B]    &   ⊢ ⊤⊧[(λx:α Sy:α) = S]    &   ⊢ [x:α = C]⊧[A = B]    &   ⊢ [x:α = C]⊧[R = S]    ⇒   ⊢ S⊧B
Theorem	insti 114*	Instantiate a theorem with a new term. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ C:α    &   ⊢ B:∗    &   ⊢ R⊧A    &   ⊢ ⊤⊧[(λx:α By:α) = B]    &   ⊢ [x:α = C]⊧[A = B]    ⇒   ⊢ R⊧B
Theorem	clf 115*	Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ C:α    &   ⊢ [x:α = C]⊧[A = B]    &   ⊢ ⊤⊧[(λx:α By:α) = B]    &   ⊢ ⊤⊧[(λx:α Cy:α) = C]    ⇒   ⊢ ⊤⊧[(λx:α AC) = B]
Theorem	cl 116*	Evaluate a lambda expression. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ C:α    &   ⊢ [x:α = C]⊧[A = B]    ⇒   ⊢ ⊤⊧[(λx:α AC) = B]
Theorem	ovl 117*	Evaluate a lambda expression in a binary operation. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:γ    &   ⊢ S:α    &   ⊢ T:β    &   ⊢ [x:α = S]⊧[A = B]    &   ⊢ [y:β = T]⊧[B = C]    ⇒   ⊢ ⊤⊧[[Sλx:α λy:β AT] = C]
0.2  Add propositional calculus definitions
Syntax	tfal 118	Contradiction term.
term ⊥
Syntax	tan 119	Conjunction term.
term ∧
Syntax	tne 120	Negation term.
term ¬
Syntax	tim 121	Implication term.
term ⇒
Syntax	tal 122	For all term.
term ∀
Syntax	tex 123	There exists term.
term ∃
Syntax	tor 124	Disjunction term.
term ∨
Syntax	teu 125	There exists unique term.
term ∃!
Definition	df-al 126*	Define the for all operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[∀ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
Definition	df-fal 127	Define the constant false. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[⊥ = (∀λp:∗ p:∗)]
Definition	df-an 128*	Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[ ∧ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
Definition	df-im 129*	Define the implication operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ ∧ q:∗] = p:∗]]
Definition	df-not 130	Define the negation operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]
Definition	df-ex 131*	Define the existence operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[∃ = λp:(α → ∗) (∀λq:∗ [(∀λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])]
Definition	df-or 132*	Define the 'or' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[ ∨ = λp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]
Definition	df-eu 133*	Define the 'exists unique' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧[∃! = λp:(α → ∗) (∃λy:α (∀λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]
Theorem	wal 134	For all type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ∀:((α → ∗) → ∗)
Theorem	wfal 135	Contradiction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊥:∗
Theorem	wan 136	Conjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ∧ :(∗ → (∗ → ∗))
Theorem	wim 137	Implication type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⇒ :(∗ → (∗ → ∗))
Theorem	wnot 138	Negation type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ¬ :(∗ → ∗)
Theorem	wex 139	There exists type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ∃:((α → ∗) → ∗)
Theorem	wor 140	Disjunction type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ∨ :(∗ → (∗ → ∗))
Theorem	weu 141	There exists unique type. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ∃!:((α → ∗) → ∗)
Theorem	alval 142*	Value of the for all predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → ∗)    ⇒   ⊢ ⊤⊧[(∀F) = [F = λx:α ⊤]]
Theorem	exval 143*	Value of the 'there exists' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → ∗)    ⇒   ⊢ ⊤⊧[(∃F) = (∀λq:∗ [(∀λx:α [(Fx:α) ⇒ q:∗]) ⇒ q:∗])]
Theorem	euval 144*	Value of the 'exists unique' predicate. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → ∗)    ⇒   ⊢ ⊤⊧[(∃!F) = (∃λy:α (∀λx:α [(Fx:α) = [x:α = y:α]]))]
Theorem	notval 145	Value of negation. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:∗    ⇒   ⊢ ⊤⊧[(¬ A) = [A ⇒ ⊥]]
Theorem	imval 146	Value of the implication. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:∗    ⇒   ⊢ ⊤⊧[[A ⇒ B] = [[A ∧ B] = A]]
Theorem	orval 147*	Value of the disjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:∗    ⇒   ⊢ ⊤⊧[[A ∨ B] = (∀λx:∗ [[A ⇒ x:∗] ⇒ [[B ⇒ x:∗] ⇒ x:∗]])]
Theorem	anval 148*	Value of the conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:∗    ⇒   ⊢ ⊤⊧[[A ∧ B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
Theorem	ax4g 149	If F is true for all x:α, then it is true for A. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ F:(α → ∗)    &   ⊢ A:α    ⇒   ⊢ (∀F)⊧(FA)
Theorem	ax4 150	If A is true for all x:α, then it is true for A. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    ⇒   ⊢ (∀λx:α A)⊧A
Theorem	alrimiv 151*	If one can prove R⊧A where R does not contain x, then A is true for all x. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ R⊧A    ⇒   ⊢ R⊧(∀λx:α A)
Theorem	cla4v 152*	If A(x) is true for all x:α, then it is true for C = A(B). (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:α    &   ⊢ [x:α = B]⊧[A = C]    ⇒   ⊢ (∀λx:α A)⊧C
Theorem	pm2.21 153	A falsehood implies anything. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    ⇒   ⊢ ⊥⊧A
Theorem	dfan2 154	An alternative definition of the "and" term in terms of the context conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:∗    ⇒   ⊢ ⊤⊧[[A ∧ B] = (A, B)]
Theorem	hbct 155	Hypothesis builder for context conjunction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:∗    &   ⊢ B:α    &   ⊢ C:∗    &   ⊢ R⊧[(λx:α AB) = A]    &   ⊢ R⊧[(λx:α CB) = C]    ⇒   ⊢ R⊧[(λx:α (A, C)B) = (A, C)]
Theorem	mpd 156	Modus ponens. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ T:∗    &   ⊢ R⊧S    &   ⊢ R⊧[S ⇒ T]    ⇒   ⊢ R⊧T
Theorem	imp 157	Importation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ S:∗    &   ⊢ T:∗    &   ⊢ R⊧[S ⇒ T]    ⇒   ⊢ (R, S)⊧T
Theorem	ex 158	Exportation deduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ (R, S)⊧T    ⇒   ⊢ R⊧[S ⇒ T]
Theorem	notval2 159	Another way two write ¬ A, the negation of A. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    ⇒   ⊢ ⊤⊧[(¬ A) = [A = ⊥]]
Theorem	notnot1 160	One side of notnot 200. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ A:∗    ⇒   ⊢ A⊧(¬ (¬ A))
Theorem	con2d 161	A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ T:∗    &   ⊢ (R, S)⊧(¬ T)    ⇒   ⊢ (R, T)⊧(¬ S)
Theorem	con3d 162	A contraposition deduction. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ (R, S)⊧T    ⇒   ⊢ (R, (¬ T))⊧(¬ S)
Theorem	ecase 163	Elimination by cases. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:∗    &   ⊢ T:∗    &   ⊢ R⊧[A ∨ B]    &   ⊢ (R, A)⊧T    &   ⊢ (R, B)⊧T    ⇒   ⊢ R⊧T
Theorem	olc 164	Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:∗    ⇒   ⊢ B⊧[A ∨ B]
Theorem	orc 165	Or introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:∗    ⇒   ⊢ A⊧[A ∨ B]
Theorem	exlimdv2 166*	Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ F:(α → ∗)    &   ⊢ (R, (Fx:α))⊧T    ⇒   ⊢ (R, (∃F))⊧T
Theorem	exlimdv 167*	Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ (R, A)⊧T    ⇒   ⊢ (R, (∃λx:α A))⊧T
Theorem	ax4e 168	Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ F:(α → ∗)    &   ⊢ A:α    ⇒   ⊢ (FA)⊧(∃F)
Theorem	cla4ev 169*	Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ B:α    &   ⊢ [x:α = B]⊧[A = C]    ⇒   ⊢ C⊧(∃λx:α A)
Theorem	19.8a 170	Existential introduction. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    ⇒   ⊢ A⊧(∃λx:α A)
0.3  Type definition mechanism
Syntax	wffMMJ2d 171	Internal axiom for mmj2 use.
wff typedef α(A, B)C
Axiom	ax-wabs 172	Type of the abstraction function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ B:α    &   ⊢ F:(α → ∗)    &   ⊢ ⊤⊧(FB)    &   ⊢ typedef β(A, R)F    ⇒   ⊢ A:(α → β)
Axiom	ax-wrep 173	Type of the representation function. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ B:α    &   ⊢ F:(α → ∗)    &   ⊢ ⊤⊧(FB)    &   ⊢ typedef β(A, R)F    ⇒   ⊢ R:(β → α)
Theorem	wabs 174	Type of the abstraction function. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ B:α    &   ⊢ F:(α → ∗)    &   ⊢ ⊤⊧(FB)    &   ⊢ typedef β(A, R)F    ⇒   ⊢ A:(α → β)
Theorem	wrep 175	Type of the representation function. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ B:α    &   ⊢ F:(α → ∗)    &   ⊢ ⊤⊧(FB)    &   ⊢ typedef β(A, R)F    ⇒   ⊢ R:(β → α)
Axiom	ax-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 A, R mapping the new type β to the subset of the old type α such that Fx 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 B that F is not always false. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ B:α    &   ⊢ F:(α → ∗)    &   ⊢ ⊤⊧(FB)    &   ⊢ typedef β(A, R)F    ⇒   ⊢ ⊤⊧((∀λx:β [(A(Rx:β)) = x:β]), (∀λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))
0.4  Extensionality
Axiom	ax-eta 177*	The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ⊤⊧(∀λf:(α → β) [λx:α (f:(α → β)x:α) = f:(α → β)])
Theorem	eta 178*	The eta-axiom: a function is determined by its values. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → β)    ⇒   ⊢ ⊤⊧[λx:α (Fx:α) = F]
Theorem	cbvf 179*	Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ ⊤⊧[(λy:α Az:α) = A]    &   ⊢ ⊤⊧[(λx:α Bz:α) = B]    &   ⊢ [x:α = y:α]⊧[A = B]    ⇒   ⊢ ⊤⊧[λx:α A = λy:α B]
Theorem	cbv 180*	Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ [x:α = y:α]⊧[A = B]    ⇒   ⊢ ⊤⊧[λx:α A = λy:α B]
Theorem	leqf 181*	Equality theorem for lambda abstraction, using bound variable instead of distinct variables. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ R⊧[A = B]    &   ⊢ ⊤⊧[(λx:α Ry:α) = R]    ⇒   ⊢ R⊧[λx:α A = λx:α B]
Theorem	alrimi 182*	If one can prove R⊧A where R does not contain x, then A is true for all x. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ R⊧A    &   ⊢ ⊤⊧[(λx:α Ry:α) = R]    ⇒   ⊢ R⊧(∀λx:α A)
Theorem	exlimd 183*	Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ (R, A)⊧T    &   ⊢ ⊤⊧[(λx:α Ry:α) = R]    &   ⊢ ⊤⊧[(λx:α Ty:α) = T]    ⇒   ⊢ (R, (∃λx:α A))⊧T
Theorem	alimdv 184*	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ (R, A)⊧B    ⇒   ⊢ (R, (∀λx:α A))⊧(∀λx:α B)
Theorem	eximdv 185*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ (R, A)⊧B    ⇒   ⊢ (R, (∃λx:α A))⊧(∃λx:α B)
Theorem	alnex 186*	Theorem 19.7 of [Margaris] p. 89. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ A:∗    ⇒   ⊢ ⊤⊧[(∀λx:α (¬ A)) = (¬ (∃λx:α A))]
Theorem	exnal1 187*	Forward direction of exnal 201. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ A:∗    ⇒   ⊢ (∃λx:α (¬ A))⊧(¬ (∀λx:α A))
Theorem	isfree 188*	Derive the metamath "is free" predicate in terms of the HOL "is free" predicate. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:∗    &   ⊢ ⊤⊧[(λx:α Ay:α) = A]    ⇒   ⊢ ⊤⊧[A ⇒ (∀λx:α A)]
0.5  Axioms of infinity and choice
Syntax	tf11 189	One-to-one function.
term 1-1
Syntax	tfo 190	Onto function.
term onto
Syntax	tat 191	Indefinite descriptor.
term ε
Axiom	ax-wat 192	The type of the indefinite descriptor. (New usage is discouraged.) (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ ε:((α → ∗) → α)
Theorem	wat 193	The type of the indefinite descriptor. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ ε:((α → ∗) → α)
Definition	df-f11 194*	Define a one-to-one function. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ ⊤⊧[1-1 = λf:(α → β) (∀λx:α (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]))]
Definition	df-fo 195*	Define an onto function. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ ⊤⊧[onto = λf:(α → β) (∀λy:β (∃λx:α [y:β = (f:(α → β)x:α)]))]
Axiom	ax-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.)
⊢ ⊤⊧(∀λp:(α → ∗) (∀λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]))
Theorem	ac 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.)
⊢ F:(α → ∗)    &   ⊢ A:α    ⇒   ⊢ (FA)⊧(F(εF))
Theorem	dfex2 198	Alternative definition of the "there exists" quantifier. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ F:(α → ∗)    ⇒   ⊢ ⊤⊧[(∃F) = (F(εF))]
Theorem	exmid 199	Diaconescu's theorem, which derives the law of the excluded middle from the axiom of choice. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ A:∗    ⇒   ⊢ ⊤⊧[A ∨ (¬ A)]
Theorem	notnot 200	Rule of double negation. (Contributed by Mario Carneiro, 10-Oct-2014.)
⊢ A:∗    ⇒   ⊢ ⊤⊧[A = (¬ (¬ A))]