Step |
Hyp |
Ref |
Expression |
1 |
|
r19.28zv |
|- ( B =/= (/) -> ( A. y e. B ( f Fn A /\ A. x e. A ( f ` x ) e. C ) <-> ( f Fn A /\ A. y e. B A. x e. A ( f ` x ) e. C ) ) ) |
2 |
|
eliin |
|- ( f e. _V -> ( f e. |^|_ y e. B X_ x e. A C <-> A. y e. B f e. X_ x e. A C ) ) |
3 |
2
|
elv |
|- ( f e. |^|_ y e. B X_ x e. A C <-> A. y e. B f e. X_ x e. A C ) |
4 |
|
vex |
|- f e. _V |
5 |
4
|
elixp |
|- ( f e. X_ x e. A C <-> ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) |
6 |
5
|
ralbii |
|- ( A. y e. B f e. X_ x e. A C <-> A. y e. B ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) |
7 |
3 6
|
bitri |
|- ( f e. |^|_ y e. B X_ x e. A C <-> A. y e. B ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) |
8 |
4
|
elixp |
|- ( f e. X_ x e. A |^|_ y e. B C <-> ( f Fn A /\ A. x e. A ( f ` x ) e. |^|_ y e. B C ) ) |
9 |
|
fvex |
|- ( f ` x ) e. _V |
10 |
|
eliin |
|- ( ( f ` x ) e. _V -> ( ( f ` x ) e. |^|_ y e. B C <-> A. y e. B ( f ` x ) e. C ) ) |
11 |
9 10
|
ax-mp |
|- ( ( f ` x ) e. |^|_ y e. B C <-> A. y e. B ( f ` x ) e. C ) |
12 |
11
|
ralbii |
|- ( A. x e. A ( f ` x ) e. |^|_ y e. B C <-> A. x e. A A. y e. B ( f ` x ) e. C ) |
13 |
|
ralcom |
|- ( A. x e. A A. y e. B ( f ` x ) e. C <-> A. y e. B A. x e. A ( f ` x ) e. C ) |
14 |
12 13
|
bitri |
|- ( A. x e. A ( f ` x ) e. |^|_ y e. B C <-> A. y e. B A. x e. A ( f ` x ) e. C ) |
15 |
14
|
anbi2i |
|- ( ( f Fn A /\ A. x e. A ( f ` x ) e. |^|_ y e. B C ) <-> ( f Fn A /\ A. y e. B A. x e. A ( f ` x ) e. C ) ) |
16 |
8 15
|
bitri |
|- ( f e. X_ x e. A |^|_ y e. B C <-> ( f Fn A /\ A. y e. B A. x e. A ( f ` x ) e. C ) ) |
17 |
1 7 16
|
3bitr4g |
|- ( B =/= (/) -> ( f e. |^|_ y e. B X_ x e. A C <-> f e. X_ x e. A |^|_ y e. B C ) ) |
18 |
17
|
eqrdv |
|- ( B =/= (/) -> |^|_ y e. B X_ x e. A C = X_ x e. A |^|_ y e. B C ) |
19 |
18
|
eqcomd |
|- ( B =/= (/) -> X_ x e. A |^|_ y e. B C = |^|_ y e. B X_ x e. A C ) |