Step |
Hyp |
Ref |
Expression |
1 |
|
mptssid.1 |
|- F/_ x A |
2 |
|
mptssid.2 |
|- C = { x e. A | B e. _V } |
3 |
|
eqvisset |
|- ( y = B -> B e. _V ) |
4 |
3
|
anim2i |
|- ( ( x e. A /\ y = B ) -> ( x e. A /\ B e. _V ) ) |
5 |
|
rabid |
|- ( x e. { x e. A | B e. _V } <-> ( x e. A /\ B e. _V ) ) |
6 |
4 5
|
sylibr |
|- ( ( x e. A /\ y = B ) -> x e. { x e. A | B e. _V } ) |
7 |
6 2
|
eleqtrrdi |
|- ( ( x e. A /\ y = B ) -> x e. C ) |
8 |
|
simpr |
|- ( ( x e. A /\ y = B ) -> y = B ) |
9 |
7 8
|
jca |
|- ( ( x e. A /\ y = B ) -> ( x e. C /\ y = B ) ) |
10 |
1
|
ssrab2f |
|- { x e. A | B e. _V } C_ A |
11 |
2 10
|
eqsstri |
|- C C_ A |
12 |
11
|
sseli |
|- ( x e. C -> x e. A ) |
13 |
12
|
anim1i |
|- ( ( x e. C /\ y = B ) -> ( x e. A /\ y = B ) ) |
14 |
9 13
|
impbii |
|- ( ( x e. A /\ y = B ) <-> ( x e. C /\ y = B ) ) |
15 |
14
|
opabbii |
|- { <. x , y >. | ( x e. A /\ y = B ) } = { <. x , y >. | ( x e. C /\ y = B ) } |
16 |
|
df-mpt |
|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) } |
17 |
|
df-mpt |
|- ( x e. C |-> B ) = { <. x , y >. | ( x e. C /\ y = B ) } |
18 |
15 16 17
|
3eqtr4i |
|- ( x e. A |-> B ) = ( x e. C |-> B ) |