Metamath Proof Explorer

Theorem dvelimf-o

Description: Proof of dvelimh that uses ax-c11 but not ax-c15 , ax-c11n , or ax-12 . Version of dvelimh using ax-c11 instead of axc11 . (Contributed by NM, 12-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvelimf-o.1 
|- ( ph -> A. x ph )
dvelimf-o.2 
|- ( ps -> A. z ps )
dvelimf-o.3 
|- ( z = y -> ( ph <-> ps ) )
Assertion dvelimf-o 
|- ( -. A. x x = y -> ( ps -> A. x ps ) )

Proof

Step Hyp Ref Expression
1 dvelimf-o.1 
 |-  ( ph -> A. x ph )
2 dvelimf-o.2 
 |-  ( ps -> A. z ps )
3 dvelimf-o.3 
 |-  ( z = y -> ( ph <-> ps ) )
4 hba1-o 
 |-  ( A. z ( z = y -> ph ) -> A. z A. z ( z = y -> ph ) )
5 ax-c11 
 |-  ( A. z z = x -> ( A. z A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
6 5 aecoms-o 
 |-  ( A. x x = z -> ( A. z A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
7 4 6 syl5 
 |-  ( A. x x = z -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
8 7 a1d 
 |-  ( A. x x = z -> ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) ) )
9 hbnae-o 
 |-  ( -. A. x x = z -> A. z -. A. x x = z )
10 hbnae-o 
 |-  ( -. A. x x = y -> A. z -. A. x x = y )
11 9 10 hban 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> A. z ( -. A. x x = z /\ -. A. x x = y ) )
12 hbnae-o 
 |-  ( -. A. x x = z -> A. x -. A. x x = z )
13 hbnae-o 
 |-  ( -. A. x x = y -> A. x -. A. x x = y )
14 12 13 hban 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> A. x ( -. A. x x = z /\ -. A. x x = y ) )
15 ax-c9 
 |-  ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
16 15 imp 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
17 1 a1i 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> ( ph -> A. x ph ) )
18 14 16 17 hbimd 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
19 11 18 hbald 
 |-  ( ( -. A. x x = z /\ -. A. x x = y ) -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
20 19 ex 
 |-  ( -. A. x x = z -> ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) ) )
21 8 20 pm2.61i 
 |-  ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
22 2 3 equsalh 
 |-  ( A. z ( z = y -> ph ) <-> ps )
23 22 albii 
 |-  ( A. x A. z ( z = y -> ph ) <-> A. x ps )
24 21 22 23 3imtr3g 
 |-  ( -. A. x x = y -> ( ps -> A. x ps ) )