Step |
Hyp |
Ref |
Expression |
1 |
|
mpofun.1 |
|- F = ( x e. A , y e. B |-> C ) |
2 |
|
eqtr3 |
|- ( ( z = C /\ w = C ) -> z = w ) |
3 |
2
|
ad2ant2l |
|- ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w ) |
4 |
3
|
gen2 |
|- A. z A. w ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w ) |
5 |
|
eqeq1 |
|- ( z = w -> ( z = C <-> w = C ) ) |
6 |
5
|
anbi2d |
|- ( z = w -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ w = C ) ) ) |
7 |
6
|
mo4 |
|- ( E* z ( ( x e. A /\ y e. B ) /\ z = C ) <-> A. z A. w ( ( ( ( x e. A /\ y e. B ) /\ z = C ) /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> z = w ) ) |
8 |
4 7
|
mpbir |
|- E* z ( ( x e. A /\ y e. B ) /\ z = C ) |
9 |
8
|
funoprab |
|- Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
10 |
|
df-mpo |
|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
11 |
1 10
|
eqtri |
|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } |
12 |
11
|
funeqi |
|- ( Fun F <-> Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } ) |
13 |
9 12
|
mpbir |
|- Fun F |