ax4g - Higher-Order Logic Explorer

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

Theorem ax4g 139

Description: If F is true for all x:α, then it is true for A.

**Hypotheses**
Ref	Expression
ax4g.1	⊢ F:(α → ∗)
ax4g.2	⊢ A:α

**Assertion**
Ref	Expression
ax4g	⊢ (∀F)⊧(FA)

Proof of Theorem ax4g Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wal 124	. . . 4 ⊢ ∀:((α → ∗) → ∗)
2		ax4g.1	. . . 4 ⊢ F:(α → ∗)
3	1, 2	wc 45	. . 3 ⊢ (∀F):∗
4	3	trud 27	. 2 ⊢ (∀F)⊧⊤
5		ax4g.2	. . . 4 ⊢ A:α
6	2, 5	wc 45	. . 3 ⊢ (FA):∗
7	4	ax-cb1 29	. . . . . 6 ⊢ (∀F):∗
8	7	id 25	. . . . 5 ⊢ (∀F)⊧(∀F)
9	2	alval 132	. . . . . 6 ⊢ ⊤⊧[(∀F) = [F = λp:α ⊤]]
10	7, 9	a1i 28	. . . . 5 ⊢ (∀F)⊧[(∀F) = [F = λp:α ⊤]]
11	8, 10	mpbi 72	. . . 4 ⊢ (∀F)⊧[F = λp:α ⊤]
12	2, 5, 11	ceq1 79	. . 3 ⊢ (∀F)⊧[(FA) = (λp:α ⊤A)]
13	5, 4	hbth 99	. . 3 ⊢ (∀F)⊧[(λp:α ⊤A) = ⊤]
14	6, 12, 13	eqtri 85	. 2 ⊢ (∀F)⊧[(FA) = ⊤]
15	4, 14	mpbir 77	1 ⊢ (∀F)⊧(FA)

Colors of variables: type var term

Syntax hints: → ht 2 ∗hb 3 kc 5 λkl 6 = ke 7 ⊤kt 8 [kbr 9 ⊧wffMMJ2 11 wffMMJ2t 12 ∀tal 112

This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-simpl 20 ax-simpr 21 ax-id 24 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ded 43 ax-ceq 46 ax-beta 60 ax-distrc 61 ax-leq 62 ax-hbl1 93 ax-17 95 ax-inst 103

This theorem depends on definitions: df-ov 65 df-al 116

This theorem is referenced by: ax4 140 cla4v 142