Step |
Hyp |
Ref |
Expression |
1 |
|
rngop.1 |
|- F = ( x e. A , y e. B |-> C ) |
2 |
|
ralrnmpo.2 |
|- ( z = C -> ( ph <-> ps ) ) |
3 |
1
|
rnmpo |
|- ran F = { w | E. x e. A E. y e. B w = C } |
4 |
3
|
raleqi |
|- ( A. z e. ran F ph <-> A. z e. { w | E. x e. A E. y e. B w = C } ph ) |
5 |
|
eqeq1 |
|- ( w = z -> ( w = C <-> z = C ) ) |
6 |
5
|
2rexbidv |
|- ( w = z -> ( E. x e. A E. y e. B w = C <-> E. x e. A E. y e. B z = C ) ) |
7 |
6
|
ralab |
|- ( A. z e. { w | E. x e. A E. y e. B w = C } ph <-> A. z ( E. x e. A E. y e. B z = C -> ph ) ) |
8 |
|
ralcom4 |
|- ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. z A. x e. A ( E. y e. B z = C -> ph ) ) |
9 |
|
r19.23v |
|- ( A. x e. A ( E. y e. B z = C -> ph ) <-> ( E. x e. A E. y e. B z = C -> ph ) ) |
10 |
9
|
albii |
|- ( A. z A. x e. A ( E. y e. B z = C -> ph ) <-> A. z ( E. x e. A E. y e. B z = C -> ph ) ) |
11 |
8 10
|
bitr2i |
|- ( A. z ( E. x e. A E. y e. B z = C -> ph ) <-> A. x e. A A. z ( E. y e. B z = C -> ph ) ) |
12 |
4 7 11
|
3bitri |
|- ( A. z e. ran F ph <-> A. x e. A A. z ( E. y e. B z = C -> ph ) ) |
13 |
|
ralcom4 |
|- ( A. y e. B A. z ( z = C -> ph ) <-> A. z A. y e. B ( z = C -> ph ) ) |
14 |
|
r19.23v |
|- ( A. y e. B ( z = C -> ph ) <-> ( E. y e. B z = C -> ph ) ) |
15 |
14
|
albii |
|- ( A. z A. y e. B ( z = C -> ph ) <-> A. z ( E. y e. B z = C -> ph ) ) |
16 |
13 15
|
bitri |
|- ( A. y e. B A. z ( z = C -> ph ) <-> A. z ( E. y e. B z = C -> ph ) ) |
17 |
|
nfv |
|- F/ z ps |
18 |
17 2
|
ceqsalg |
|- ( C e. V -> ( A. z ( z = C -> ph ) <-> ps ) ) |
19 |
18
|
ralimi |
|- ( A. y e. B C e. V -> A. y e. B ( A. z ( z = C -> ph ) <-> ps ) ) |
20 |
|
ralbi |
|- ( A. y e. B ( A. z ( z = C -> ph ) <-> ps ) -> ( A. y e. B A. z ( z = C -> ph ) <-> A. y e. B ps ) ) |
21 |
19 20
|
syl |
|- ( A. y e. B C e. V -> ( A. y e. B A. z ( z = C -> ph ) <-> A. y e. B ps ) ) |
22 |
16 21
|
bitr3id |
|- ( A. y e. B C e. V -> ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) ) |
23 |
22
|
ralimi |
|- ( A. x e. A A. y e. B C e. V -> A. x e. A ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) ) |
24 |
|
ralbi |
|- ( A. x e. A ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) -> ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. x e. A A. y e. B ps ) ) |
25 |
23 24
|
syl |
|- ( A. x e. A A. y e. B C e. V -> ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. x e. A A. y e. B ps ) ) |
26 |
12 25
|
bitrid |
|- ( A. x e. A A. y e. B C e. V -> ( A. z e. ran F ph <-> A. x e. A A. y e. B ps ) ) |