Metamath Proof Explorer

Theorem eu6w

Description: Replace ax-10 , ax-12 in eu6 with substitution hypotheses. (Contributed by SN, 27-May-2025)

Ref Expression
Hypotheses eu6w.x 
|- ( x = z -> ( ph <-> ps ) )
eu6w.y 
|- ( x = y -> ( ph <-> th ) )
Assertion eu6w 
|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )

Proof

Step Hyp Ref Expression
1 eu6w.x 
 |-  ( x = z -> ( ph <-> ps ) )
2 eu6w.y 
 |-  ( x = y -> ( ph <-> th ) )
3 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
4 pm2.21 
 |-  ( -. ph -> ( ph -> x = y ) )
5 4 alimi 
 |-  ( A. x -. ph -> A. x ( ph -> x = y ) )
6 3 5 sylbir 
 |-  ( -. E. x ph -> A. x ( ph -> x = y ) )
7 equequ2 
 |-  ( y = z -> ( x = y <-> x = z ) )
8 7 imbi2d 
 |-  ( y = z -> ( ( ph -> x = y ) <-> ( ph -> x = z ) ) )
9 8 albidv 
 |-  ( y = z -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = z ) ) )
10 9 19.8aw 
 |-  ( A. x ( ph -> x = y ) -> E. y A. x ( ph -> x = y ) )
11 6 10 syl 
 |-  ( -. E. x ph -> E. y A. x ( ph -> x = y ) )
12 biimp 
 |-  ( ( ph <-> x = y ) -> ( ph -> x = y ) )
13 12 alimi 
 |-  ( A. x ( ph <-> x = y ) -> A. x ( ph -> x = y ) )
14 13 eximi 
 |-  ( E. y A. x ( ph <-> x = y ) -> E. y A. x ( ph -> x = y ) )
15 11 14 ja 
 |-  ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) -> E. y A. x ( ph -> x = y ) )
16 equequ1 
 |-  ( x = z -> ( x = y <-> z = y ) )
17 1 16 imbi12d 
 |-  ( x = z -> ( ( ph -> x = y ) <-> ( ps -> z = y ) ) )
18 17 nfa1w 
 |-  F/ x A. x ( ph -> x = y )
19 1 16 bibi12d 
 |-  ( x = z -> ( ( ph <-> x = y ) <-> ( ps <-> z = y ) ) )
20 19 nfa1w 
 |-  F/ x A. x ( ph <-> x = y )
21 18 20 nfim 
 |-  F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) )
22 19.38b 
 |-  ( F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> ( ( E. x ph -> A. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) <-> A. x ( ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) ) )
23 17 cbvalvw 
 |-  ( A. x ( ph -> x = y ) <-> A. z ( ps -> z = y ) )
24 19 cbvalvw 
 |-  ( A. x ( ph <-> x = y ) <-> A. z ( ps <-> z = y ) )
25 23 24 imbi12i 
 |-  ( ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) <-> ( A. z ( ps -> z = y ) -> A. z ( ps <-> z = y ) ) )
26 25 a1i 
 |-  ( x = z -> ( ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) <-> ( A. z ( ps -> z = y ) -> A. z ( ps <-> z = y ) ) ) )
27 26 spw 
 |-  ( A. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
28 26 19.8aw 
 |-  ( ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> E. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
29 id 
 |-  ( F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
30 29 nfrd 
 |-  ( F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> ( E. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> A. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) )
31 28 30 syl5 
 |-  ( F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> ( ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> A. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) )
32 27 31 impbid2 
 |-  ( F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> ( A. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) <-> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) )
33 32 imbi2d 
 |-  ( F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> ( ( E. x ph -> A. x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) <-> ( E. x ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) ) )
34 22 33 bitr3d 
 |-  ( F/ x ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) -> ( A. x ( ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) <-> ( E. x ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) ) )
35 21 34 ax-mp 
 |-  ( A. x ( ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) <-> ( E. x ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) ) )
36 17 spw 
 |-  ( A. x ( ph -> x = y ) -> ( ph -> x = y ) )
37 id 
 |-  ( ph -> ph )
38 2 ax12wlem 
 |-  ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
39 38 com12 
 |-  ( ph -> ( x = y -> A. x ( x = y -> ph ) ) )
40 37 39 embantd 
 |-  ( ph -> ( ( ph -> x = y ) -> A. x ( x = y -> ph ) ) )
41 36 40 syl5 
 |-  ( ph -> ( A. x ( ph -> x = y ) -> A. x ( x = y -> ph ) ) )
42 41 ancld 
 |-  ( ph -> ( A. x ( ph -> x = y ) -> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) ) )
43 albiim 
 |-  ( A. x ( ph <-> x = y ) <-> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) )
44 42 43 imbitrrdi 
 |-  ( ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
45 35 44 mpgbi 
 |-  ( E. x ph -> ( A. x ( ph -> x = y ) -> A. x ( ph <-> x = y ) ) )
46 45 eximdv 
 |-  ( E. x ph -> ( E. y A. x ( ph -> x = y ) -> E. y A. x ( ph <-> x = y ) ) )
47 46 com12 
 |-  ( E. y A. x ( ph -> x = y ) -> ( E. x ph -> E. y A. x ( ph <-> x = y ) ) )
48 15 47 impbii 
 |-  ( ( E. x ph -> E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph -> x = y ) )
49 48 anbi2i 
 |-  ( ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
50 abai 
 |-  ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. x ph /\ ( E. x ph -> E. y A. x ( ph <-> x = y ) ) ) )
51 eu3v 
 |-  ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
52 49 50 51 3bitr4ri 
 |-  ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) )
53 abai 
 |-  ( ( E. y A. x ( ph <-> x = y ) /\ E. x ph ) <-> ( E. y A. x ( ph <-> x = y ) /\ ( E. y A. x ( ph <-> x = y ) -> E. x ph ) ) )
54 ancom 
 |-  ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> ( E. y A. x ( ph <-> x = y ) /\ E. x ph ) )
55 biimpr 
 |-  ( ( ph <-> x = y ) -> ( x = y -> ph ) )
56 55 alimi 
 |-  ( A. x ( ph <-> x = y ) -> A. x ( x = y -> ph ) )
57 56 eximi 
 |-  ( E. y A. x ( ph <-> x = y ) -> E. y A. x ( x = y -> ph ) )
58 exsbim 
 |-  ( E. y A. x ( x = y -> ph ) -> E. x ph )
59 57 58 syl 
 |-  ( E. y A. x ( ph <-> x = y ) -> E. x ph )
60 59 biantru 
 |-  ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( ph <-> x = y ) /\ ( E. y A. x ( ph <-> x = y ) -> E. x ph ) ) )
61 53 54 60 3bitr4i 
 |-  ( ( E. x ph /\ E. y A. x ( ph <-> x = y ) ) <-> E. y A. x ( ph <-> x = y ) )
62 52 61 bitri 
 |-  ( E! x ph <-> E. y A. x ( ph <-> x = y ) )