Theorem dvelimf-o 32469

Description: Proof of dvelimh 2137 that uses ax-c11 32428 but not ax-c15 32430, ax-c11n 32429, or ax-12 1909. Version of dvelimh 2137 using ax-c11 32428 instead of axc11 2113. (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 32438	. . . . 5 |- ( A. z ( z = y -> ph ) -> A. z A. z ( z = y -> ph ) )
2		ax-c11 32428	. . . . . 6 |- ( A. z z = x -> ( A. z A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
3	2	aecoms-o 32441	. . . . 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 32468	. . . . . 6 |- ( -. A. x x = z -> A. z -. A. x x = z )
7		hbnae-o 32468	. . . . . 6 |- ( -. A. x x = y -> A. z -. A. x x = y )
8	6, 7	hban 1991	. . . . 5 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> A. z ( -. A. x x = z /\ -. A. x x = y ) )
9		hbnae-o 32468	. . . . . . 7 |- ( -. A. x x = z -> A. x -. A. x x = z )
10		hbnae-o 32468	. . . . . . 7 |- ( -. A. x x = y -> A. x -. A. x x = y )
11	9, 10	hban 1991	. . . . . 6 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> A. x ( -. A. x x = z /\ -. A. x x = y ) )
12		ax-c9 32431	. . . . . . 7 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
13	12	imp 430	. . . . . 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 1981	. . . . 5 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
17	8, 16	hbald 1902	. . . 4 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
18	17	ex 435	. . 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 167	. 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 2094	. 2 |- ( A. z ( z = y -> ph ) <-> ps )
23	22	albii 1685	. 2 |- ( A. x A. z ( z = y -> ph ) <-> A. x ps )
24	19, 22, 23	3imtr3g 272	1 |- ( -. A. x x = y -> ( ps -> A. x ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-c5 32424  ax-c4 32425  ax-c7 32426  ax-c11 32428  ax-c9 32431

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-nf 1662

This theorem is referenced by:  dveeq2-o  32473  dveeq1-o  32475  ax12el  32482