Theorem dvelimf-o 34214

Description: Proof of dvelimh 2336 that uses ax-c11 34172 but not ax-c15 34174, ax-c11n 34173, or ax-12 2047. Version of dvelimh 2336 using ax-c11 34172 instead of axc11 2314. (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 34182	. . . . 5 |- ( A. z ( z = y -> ph ) -> A. z A. z ( z = y -> ph ) )
2		ax-c11 34172	. . . . . 6 |- ( A. z z = x -> ( A. z A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
3	2	aecoms-o 34187	. . . . 5 |- ( A. x x = z -> ( A. z A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
4	1, 3	syl5 34	. . . 4 |- ( A. x x = z -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
5	4	a1d 25	. . 3 |- ( A. x x = z -> ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) ) )
6		hbnae-o 34213	. . . . . 6 |- ( -. A. x x = z -> A. z -. A. x x = z )
7		hbnae-o 34213	. . . . . 6 |- ( -. A. x x = y -> A. z -. A. x x = y )
8	6, 7	hban 2128	. . . . 5 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> A. z ( -. A. x x = z /\ -. A. x x = y ) )
9		hbnae-o 34213	. . . . . . 7 |- ( -. A. x x = z -> A. x -. A. x x = z )
10		hbnae-o 34213	. . . . . . 7 |- ( -. A. x x = y -> A. x -. A. x x = y )
11	9, 10	hban 2128	. . . . . 6 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> A. x ( -. A. x x = z /\ -. A. x x = y ) )
12		ax-c9 34175	. . . . . . 7 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
13	12	imp 445	. . . . . 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 2126	. . . . 5 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
17	8, 16	hbald 2041	. . . 4 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
18	17	ex 450	. . 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 176	. 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 2294	. 2 |- ( A. z ( z = y -> ph ) <-> ps )
23	22	albii 1747	. 2 |- ( A. x A. z ( z = y -> ph ) <-> A. x ps )
24	19, 22, 23	3imtr3g 284	1 |- ( -. A. x x = y -> ( ps -> A. x ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-c5 34168  ax-c4 34169  ax-c7 34170  ax-c10 34171  ax-c11 34172  ax-c9 34175

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by:  dveeq2-o  34218  dveeq1-o  34220  ax12el  34227