Step |
Hyp |
Ref |
Expression |
1 |
|
fneq2 |
|- ( A = B -> ( f Fn A <-> f Fn B ) ) |
2 |
|
raleq |
|- ( A = B -> ( A. x e. A ( f ` x ) e. C <-> A. x e. B ( f ` x ) e. C ) ) |
3 |
1 2
|
anbi12d |
|- ( A = B -> ( ( f Fn A /\ A. x e. A ( f ` x ) e. C ) <-> ( f Fn B /\ A. x e. B ( f ` x ) e. C ) ) ) |
4 |
3
|
abbidv |
|- ( A = B -> { f | ( f Fn A /\ A. x e. A ( f ` x ) e. C ) } = { f | ( f Fn B /\ A. x e. B ( f ` x ) e. C ) } ) |
5 |
|
dfixp |
|- X_ x e. A C = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. C ) } |
6 |
|
dfixp |
|- X_ x e. B C = { f | ( f Fn B /\ A. x e. B ( f ` x ) e. C ) } |
7 |
4 5 6
|
3eqtr4g |
|- ( A = B -> X_ x e. A C = X_ x e. B C ) |