Theorem ax11a2 1216

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

Hypothesis

Ref	Expression
ax11a2.1	|- (x = z -> (A.zph -> A.x(x = z -> ph)))

Assertion

Ref	Expression
ax11a2	|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))

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

Proof of Theorem ax11a2

Step	Hyp	Ref	Expression
1		ax11a2.1	. . 3 |- (x = z -> (A.zph -> A.x(x = z -> ph)))
2		ax-17 971	. . 3 |- (ph -> A.zph)
3	1, 2	syl5 21	. 2 |- (x = z -> (ph -> A.x(x = z -> ph)))
4	3	ax11v2 1215	1 |- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))

Syntax hints:  -. wn 2   -> wi 3  A.wal 954   = wceq 956

This theorem is referenced by:  ax11o 1217

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140

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

Copyright terms: Public domain