Theorem ax11a2 1214

Description: Derive ax-11o 1216 from a hypothesis in the form of ax-11 965. The hypothesis is even weaker than ax-11 965, 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 1215. As theorem ax11 1217 shows, the distinct variable conditions are optional. An open problem is whether ax11o 1215 can be derived from ax-11 965 without relying on ax-17 969.

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 969	. . 3 |- (ph -> A.zph)
3	1, 2	syl5 21	. 2 |- (x = z -> (ph -> A.x(x = z -> ph)))
4	3	ax11v2 1213	1 |- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))

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

This theorem is referenced by:  ax11o 1215

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138

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

Copyright terms: Public domain