Step |
Hyp |
Ref |
Expression |
1 |
|
an4 |
|- ( ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) /\ ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) <-> ( ( f Fn A /\ f Fn A ) /\ ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) ) ) |
2 |
|
anidm |
|- ( ( f Fn A /\ f Fn A ) <-> f Fn A ) |
3 |
|
r19.26 |
|- ( A. x e. A ( ( f ` x ) e. B /\ ( f ` x ) e. C ) <-> ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) ) |
4 |
|
elin |
|- ( ( f ` x ) e. ( B i^i C ) <-> ( ( f ` x ) e. B /\ ( f ` x ) e. C ) ) |
5 |
4
|
bicomi |
|- ( ( ( f ` x ) e. B /\ ( f ` x ) e. C ) <-> ( f ` x ) e. ( B i^i C ) ) |
6 |
5
|
ralbii |
|- ( A. x e. A ( ( f ` x ) e. B /\ ( f ` x ) e. C ) <-> A. x e. A ( f ` x ) e. ( B i^i C ) ) |
7 |
3 6
|
bitr3i |
|- ( ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) <-> A. x e. A ( f ` x ) e. ( B i^i C ) ) |
8 |
2 7
|
anbi12i |
|- ( ( ( f Fn A /\ f Fn A ) /\ ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( f ` x ) e. C ) ) <-> ( f Fn A /\ A. x e. A ( f ` x ) e. ( B i^i C ) ) ) |
9 |
1 8
|
bitri |
|- ( ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) /\ ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) <-> ( f Fn A /\ A. x e. A ( f ` x ) e. ( B i^i C ) ) ) |
10 |
|
vex |
|- f e. _V |
11 |
10
|
elixp |
|- ( f e. X_ x e. A B <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) ) |
12 |
10
|
elixp |
|- ( f e. X_ x e. A C <-> ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) |
13 |
11 12
|
anbi12i |
|- ( ( f e. X_ x e. A B /\ f e. X_ x e. A C ) <-> ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) /\ ( f Fn A /\ A. x e. A ( f ` x ) e. C ) ) ) |
14 |
10
|
elixp |
|- ( f e. X_ x e. A ( B i^i C ) <-> ( f Fn A /\ A. x e. A ( f ` x ) e. ( B i^i C ) ) ) |
15 |
9 13 14
|
3bitr4i |
|- ( ( f e. X_ x e. A B /\ f e. X_ x e. A C ) <-> f e. X_ x e. A ( B i^i C ) ) |
16 |
15
|
ineqri |
|- ( X_ x e. A B i^i X_ x e. A C ) = X_ x e. A ( B i^i C ) |