Theorem ax4g 149

Description: If F is true for all x:α, then it is true for A. (Contributed by Mario Carneiro, 9-Oct-2014.)

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 134	. . . 4 ⊢ ∀:((α → ∗) → ∗)
2		ax4g.1	. . . 4 ⊢ F:(α → ∗)
3	1, 2	wc 50	. . 3 ⊢ (∀F):∗
4	3	trud 27	. 2 ⊢ (∀F)⊧⊤
5		ax4g.2	. . . 4 ⊢ A:α
6	2, 5	wc 50	. . 3 ⊢ (FA):∗
7	4	ax-cb1 29	. . . . . 6 ⊢ (∀F):∗
8	7	id 25	. . . . 5 ⊢ (∀F)⊧(∀F)
9	2	alval 142	. . . . . 6 ⊢ ⊤⊧[(∀F) = [F = λp:α ⊤]]
10	7, 9	a1i 28	. . . . 5 ⊢ (∀F)⊧[(∀F) = [F = λp:α ⊤]]
11	8, 10	mpbi 82	. . . 4 ⊢ (∀F)⊧[F = λp:α ⊤]
12	2, 5, 11	ceq1 89	. . 3 ⊢ (∀F)⊧[(FA) = (λp:α ⊤A)]
13	5, 4	hbth 109	. . 3 ⊢ (∀F)⊧[(λp:α ⊤A) = ⊤]
14	6, 12, 13	eqtri 95	. 2 ⊢ (∀F)⊧[(FA) = ⊤]
15	4, 14	mpbir 87	1 ⊢ (∀F)⊧(FA)

This proof depends on syntax axioms:   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12  ∀tal 122

This proof depends on 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-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wv 63  ax-wl 65  ax-beta 67  ax-distrc 68  ax-leq 69  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80  ax-hbl1 103  ax-17 105  ax-inst 113

This proof depends on definitions:  df-ov 73  df-al 126

This theorem is used by:  ax4  150  cla4v  152