This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax12inda

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Quantification case. (When z and y are distinct, ax12inda2 may be used instead to avoid the dummy variable w in the proof.) (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12inda.1 
|- ( -. A. x x = w -> ( x = w -> ( ph -> A. x ( x = w -> ph ) ) ) )
Assertion ax12inda 
|- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )

Proof

Step Hyp Ref Expression
1 ax12inda.1 
 |-  ( -. A. x x = w -> ( x = w -> ( ph -> A. x ( x = w -> ph ) ) ) )
2 ax6ev 
 |-  E. w w = y
3 1 ax12inda2 
 |-  ( -. A. x x = w -> ( x = w -> ( A. z ph -> A. x ( x = w -> A. z ph ) ) ) )
4 dveeq2-o 
 |-  ( -. A. x x = y -> ( w = y -> A. x w = y ) )
5 4 imp 
 |-  ( ( -. A. x x = y /\ w = y ) -> A. x w = y )
6 hba1-o 
 |-  ( A. x w = y -> A. x A. x w = y )
7 equequ2 
 |-  ( w = y -> ( x = w <-> x = y ) )
8 7 sps-o 
 |-  ( A. x w = y -> ( x = w <-> x = y ) )
9 6 8 albidh 
 |-  ( A. x w = y -> ( A. x x = w <-> A. x x = y ) )
10 9 notbid 
 |-  ( A. x w = y -> ( -. A. x x = w <-> -. A. x x = y ) )
11 5 10 syl 
 |-  ( ( -. A. x x = y /\ w = y ) -> ( -. A. x x = w <-> -. A. x x = y ) )
12 7 adantl 
 |-  ( ( -. A. x x = y /\ w = y ) -> ( x = w <-> x = y ) )
13 8 imbi1d 
 |-  ( A. x w = y -> ( ( x = w -> A. z ph ) <-> ( x = y -> A. z ph ) ) )
14 6 13 albidh 
 |-  ( A. x w = y -> ( A. x ( x = w -> A. z ph ) <-> A. x ( x = y -> A. z ph ) ) )
15 5 14 syl 
 |-  ( ( -. A. x x = y /\ w = y ) -> ( A. x ( x = w -> A. z ph ) <-> A. x ( x = y -> A. z ph ) ) )
16 15 imbi2d 
 |-  ( ( -. A. x x = y /\ w = y ) -> ( ( A. z ph -> A. x ( x = w -> A. z ph ) ) <-> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
17 12 16 imbi12d 
 |-  ( ( -. A. x x = y /\ w = y ) -> ( ( x = w -> ( A. z ph -> A. x ( x = w -> A. z ph ) ) ) <-> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
18 11 17 imbi12d 
 |-  ( ( -. A. x x = y /\ w = y ) -> ( ( -. A. x x = w -> ( x = w -> ( A. z ph -> A. x ( x = w -> A. z ph ) ) ) ) <-> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) ) )
19 3 18 mpbii 
 |-  ( ( -. A. x x = y /\ w = y ) -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
20 19 ex 
 |-  ( -. A. x x = y -> ( w = y -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) ) )
21 20 exlimdv 
 |-  ( -. A. x x = y -> ( E. w w = y -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) ) )
22 2 21 mpi 
 |-  ( -. A. x x = y -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
23 22 pm2.43i 
 |-  ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )