Step |
Hyp |
Ref |
Expression |
1 |
|
eumo |
|- ( E! z ps -> E* z ps ) |
2 |
1
|
imim2i |
|- ( ( ph -> E! z ps ) -> ( ph -> E* z ps ) ) |
3 |
|
moanimv |
|- ( E* z ( ph /\ ps ) <-> ( ph -> E* z ps ) ) |
4 |
2 3
|
sylibr |
|- ( ( ph -> E! z ps ) -> E* z ( ph /\ ps ) ) |
5 |
4
|
2alimi |
|- ( A. x A. y ( ph -> E! z ps ) -> A. x A. y E* z ( ph /\ ps ) ) |
6 |
|
funoprabg |
|- ( A. x A. y E* z ( ph /\ ps ) -> Fun { <. <. x , y >. , z >. | ( ph /\ ps ) } ) |
7 |
5 6
|
syl |
|- ( A. x A. y ( ph -> E! z ps ) -> Fun { <. <. x , y >. , z >. | ( ph /\ ps ) } ) |
8 |
|
dmoprab |
|- dom { <. <. x , y >. , z >. | ( ph /\ ps ) } = { <. x , y >. | E. z ( ph /\ ps ) } |
9 |
|
nfa1 |
|- F/ x A. x A. y ( ph -> E! z ps ) |
10 |
|
nfa2 |
|- F/ y A. x A. y ( ph -> E! z ps ) |
11 |
|
simpl |
|- ( ( ph /\ ps ) -> ph ) |
12 |
11
|
exlimiv |
|- ( E. z ( ph /\ ps ) -> ph ) |
13 |
|
euex |
|- ( E! z ps -> E. z ps ) |
14 |
13
|
imim2i |
|- ( ( ph -> E! z ps ) -> ( ph -> E. z ps ) ) |
15 |
14
|
ancld |
|- ( ( ph -> E! z ps ) -> ( ph -> ( ph /\ E. z ps ) ) ) |
16 |
|
19.42v |
|- ( E. z ( ph /\ ps ) <-> ( ph /\ E. z ps ) ) |
17 |
15 16
|
syl6ibr |
|- ( ( ph -> E! z ps ) -> ( ph -> E. z ( ph /\ ps ) ) ) |
18 |
12 17
|
impbid2 |
|- ( ( ph -> E! z ps ) -> ( E. z ( ph /\ ps ) <-> ph ) ) |
19 |
18
|
sps |
|- ( A. y ( ph -> E! z ps ) -> ( E. z ( ph /\ ps ) <-> ph ) ) |
20 |
19
|
sps |
|- ( A. x A. y ( ph -> E! z ps ) -> ( E. z ( ph /\ ps ) <-> ph ) ) |
21 |
9 10 20
|
opabbid |
|- ( A. x A. y ( ph -> E! z ps ) -> { <. x , y >. | E. z ( ph /\ ps ) } = { <. x , y >. | ph } ) |
22 |
8 21
|
eqtrid |
|- ( A. x A. y ( ph -> E! z ps ) -> dom { <. <. x , y >. , z >. | ( ph /\ ps ) } = { <. x , y >. | ph } ) |
23 |
|
df-fn |
|- ( { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } <-> ( Fun { <. <. x , y >. , z >. | ( ph /\ ps ) } /\ dom { <. <. x , y >. , z >. | ( ph /\ ps ) } = { <. x , y >. | ph } ) ) |
24 |
7 22 23
|
sylanbrc |
|- ( A. x A. y ( ph -> E! z ps ) -> { <. <. x , y >. , z >. | ( ph /\ ps ) } Fn { <. x , y >. | ph } ) |