Step |
Hyp |
Ref |
Expression |
1 |
|
relco |
|- Rel ( A o. B ) |
2 |
|
reliun |
|- ( Rel U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> A. x e. _V Rel ( ( `' B " { x } ) X. ( A " { x } ) ) ) |
3 |
|
relxp |
|- Rel ( ( `' B " { x } ) X. ( A " { x } ) ) |
4 |
3
|
a1i |
|- ( x e. _V -> Rel ( ( `' B " { x } ) X. ( A " { x } ) ) ) |
5 |
2 4
|
mprgbir |
|- Rel U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) |
6 |
|
opelco2g |
|- ( ( y e. _V /\ z e. _V ) -> ( <. y , z >. e. ( A o. B ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) ) ) |
7 |
6
|
el2v |
|- ( <. y , z >. e. ( A o. B ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) ) |
8 |
|
eliun |
|- ( <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x e. _V <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) ) |
9 |
|
rexv |
|- ( E. x e. _V <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) ) |
10 |
|
opelxp |
|- ( <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> ( y e. ( `' B " { x } ) /\ z e. ( A " { x } ) ) ) |
11 |
|
vex |
|- x e. _V |
12 |
|
vex |
|- y e. _V |
13 |
11 12
|
elimasn |
|- ( y e. ( `' B " { x } ) <-> <. x , y >. e. `' B ) |
14 |
11 12
|
opelcnv |
|- ( <. x , y >. e. `' B <-> <. y , x >. e. B ) |
15 |
13 14
|
bitri |
|- ( y e. ( `' B " { x } ) <-> <. y , x >. e. B ) |
16 |
|
vex |
|- z e. _V |
17 |
11 16
|
elimasn |
|- ( z e. ( A " { x } ) <-> <. x , z >. e. A ) |
18 |
15 17
|
anbi12i |
|- ( ( y e. ( `' B " { x } ) /\ z e. ( A " { x } ) ) <-> ( <. y , x >. e. B /\ <. x , z >. e. A ) ) |
19 |
10 18
|
bitri |
|- ( <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> ( <. y , x >. e. B /\ <. x , z >. e. A ) ) |
20 |
19
|
exbii |
|- ( E. x <. y , z >. e. ( ( `' B " { x } ) X. ( A " { x } ) ) <-> E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) ) |
21 |
8 9 20
|
3bitrri |
|- ( E. x ( <. y , x >. e. B /\ <. x , z >. e. A ) <-> <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) ) |
22 |
7 21
|
bitri |
|- ( <. y , z >. e. ( A o. B ) <-> <. y , z >. e. U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) ) |
23 |
1 5 22
|
eqrelriiv |
|- ( A o. B ) = U_ x e. _V ( ( `' B " { x } ) X. ( A " { x } ) ) |