Theorem ax11a2 1220

Description: Derive ax-11o 1222 from a hypothesis in the form of ax-11 971. The hypothesis is even weaker than ax-11 971, with z both distinct from x and not occurring in φ. Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1221. As theorem ax11 1223 shows, the distinct variable conditions are optional. An open problem is whether ax11o 1221 can be derived from ax-11 971 without relying on ax-17 975.

Hypothesis

Ref	Expression
ax11a2.1	⊢ (x = z → (∀zφ → ∀x(x = z → φ)))

Assertion

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

Distinct variable groups:   x,z   y,z   φ,z

Proof of Theorem ax11a2

Step	Hyp	Ref	Expression
1		ax11a2.1	. . 3 ⊢ (x = z → (∀zφ → ∀x(x = z → φ)))
2		ax-17 975	. . 3 ⊢ (φ → ∀zφ)
3	1, 2	syl5 21	. 2 ⊢ (x = z → (φ → ∀x(x = z → φ)))
4	3	ax11v2 1219	1 ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))

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

This theorem is referenced by:  ax11o 1221

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985

Copyright terms: Public domain