Metamath Proof Explorer


Theorem ax12i

Description: Inference that has ax-12 (without A. y ) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without using ax-12 in special cases. Proof similar to Lemma 16 of Tarski p. 70. (Contributed by NM, 20-May-2008)

Ref Expression
Hypotheses ax12i.1
|- ( x = y -> ( ph <-> ps ) )
ax12i.2
|- ( ps -> A. x ps )
Assertion ax12i
|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )

Proof

Step Hyp Ref Expression
1 ax12i.1
 |-  ( x = y -> ( ph <-> ps ) )
2 ax12i.2
 |-  ( ps -> A. x ps )
3 1 biimprcd
 |-  ( ps -> ( x = y -> ph ) )
4 2 3 alrimih
 |-  ( ps -> A. x ( x = y -> ph ) )
5 1 4 syl6bi
 |-  ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )