Theorem dvelimf-o 32545

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

Hypotheses

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

Assertion

Ref	Expression
dvelimf-o	|- ( -. A. x x = y -> ( ps -> A. x ps ) )

Proof of Theorem dvelimf-o

Step	Hyp	Ref	Expression
1		hba1-o 32514	. . . . 5 |- ( A. z ( z = y -> ph ) -> A. z A. z ( z = y -> ph ) )
2		ax-c11 32504	. . . . . 6 |- ( A. z z = x -> ( A. z A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
3	2	aecoms-o 32517	. . . . 5 |- ( A. x x = z -> ( A. z A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
4	1, 3	syl5 33	. . . 4 |- ( A. x x = z -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
5	4	a1d 26	. . 3 |- ( A. x x = z -> ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) ) )
6		hbnae-o 32544	. . . . . 6 |- ( -. A. x x = z -> A. z -. A. x x = z )
7		hbnae-o 32544	. . . . . 6 |- ( -. A. x x = y -> A. z -. A. x x = y )
8	6, 7	hban 2025	. . . . 5 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> A. z ( -. A. x x = z /\ -. A. x x = y ) )
9		hbnae-o 32544	. . . . . . 7 |- ( -. A. x x = z -> A. x -. A. x x = z )
10		hbnae-o 32544	. . . . . . 7 |- ( -. A. x x = y -> A. x -. A. x x = y )
11	9, 10	hban 2025	. . . . . 6 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> A. x ( -. A. x x = z /\ -. A. x x = y ) )
12		ax-c9 32507	. . . . . . 7 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
13	12	imp 435	. . . . . 6 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
14		dvelimf-o.1	. . . . . . 7 |- ( ph -> A. x ph )
15	14	a1i 11	. . . . . 6 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( ph -> A. x ph ) )
16	11, 13, 15	hbimd 2015	. . . . 5 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
17	8, 16	hbald 1937	. . . 4 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
18	17	ex 440	. . 3 |- ( -. A. x x = z -> ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) ) )
19	5, 18	pm2.61i 169	. 2 |- ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
20		dvelimf-o.2	. . 3 |- ( ps -> A. z ps )
21		dvelimf-o.3	. . 3 |- ( z = y -> ( ph <-> ps ) )
22	20, 21	equsalh 2140	. 2 |- ( A. z ( z = y -> ph ) <-> ps )
23	22	albii 1702	. 2 |- ( A. x A. z ( z = y -> ph ) <-> A. x ps )
24	19, 22, 23	3imtr3g 277	1 |- ( -. A. x x = y -> ( ps -> A. x ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   A.wal 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-c5 32500  ax-c4 32501  ax-c7 32502  ax-c11 32504  ax-c9 32507

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679

This theorem is referenced by:  dveeq2-o  32549  dveeq1-o  32551  ax12el  32558