Theorem ax11f 1367

Description: Basis step for constructing a substitution instance of ax-11o 1220 without using ax-11o 1220. We can start with any formula φ in which x is not free.

Hypothesis

Ref	Expression
ax11f.1	⊢ (φ → ∀xφ)

Assertion

Ref	Expression
ax11f	⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))

Proof of Theorem ax11f

Step	Hyp	Ref	Expression
1		ax11f.1	. . . 4 ⊢ (φ → ∀xφ)
2		ax-1 4	. . . 4 ⊢ (φ → (x = y → φ))
3	1, 2	19.21ai 1000	. . 3 ⊢ (φ → ∀x(x = y → φ))
4	3	a1i 8	. 2 ⊢ (x = y → (φ → ∀x(x = y → φ)))
5	4	a1i 8	1 ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 956   = wceq 958

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977

Copyright terms: Public domain