beta - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > beta		GIF version

Theorem beta 82

Description: Axiom of beta-substitution.

**Hypothesis**
Ref	Expression
beta.1	⊢ A:β

**Assertion**
Ref	Expression
beta	⊢ ⊤⊧[(λx:α Ax:α) = A]

**Proof of Theorem beta**
Step	Hyp	Ref	Expression
1		weq 38	. 2 ⊢ = :(β → (β → ∗))
2		beta.1	. . . 4 ⊢ A:β
3	2	wl 59	. . 3 ⊢ λx:α A:(α → β)
4		wv 58	. . 3 ⊢ x:α:α
5	3, 4	wc 45	. 2 ⊢ (λx:α Ax:α):β
6	2	ax-beta 60	. 2 ⊢ ⊤⊧(( = (λx:α Ax:α))A)
7	1, 5, 2, 6	dfov2 67	1 ⊢ ⊤⊧[(λx:α Ax:α) = A]

Colors of variables: type var term

Syntax hints: tv 1 kc 5 λkl 6 = ke 7 ⊤kt 8 [kbr 9 ⊧wffMMJ2 11 wffMMJ2t 12

This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ceq 46 ax-beta 60

This theorem depends on definitions: df-ov 65

This theorem is referenced by: clf 105 ax4 140 exlimdv 157 19.8a 160 cbvf 167 leqf 169 exlimd 171 ax11 201 axrep 207