| Step |
Hyp |
Ref |
Expression |
| 1 |
|
brbigcup.1 |
|- B e. _V |
| 2 |
|
relbigcup |
|- Rel Bigcup |
| 3 |
2
|
brrelex1i |
|- ( A Bigcup B -> A e. _V ) |
| 4 |
|
eleq1 |
|- ( U. A = B -> ( U. A e. _V <-> B e. _V ) ) |
| 5 |
1 4
|
mpbiri |
|- ( U. A = B -> U. A e. _V ) |
| 6 |
|
uniexb |
|- ( A e. _V <-> U. A e. _V ) |
| 7 |
5 6
|
sylibr |
|- ( U. A = B -> A e. _V ) |
| 8 |
|
breq1 |
|- ( x = A -> ( x Bigcup B <-> A Bigcup B ) ) |
| 9 |
|
unieq |
|- ( x = A -> U. x = U. A ) |
| 10 |
9
|
eqeq1d |
|- ( x = A -> ( U. x = B <-> U. A = B ) ) |
| 11 |
|
vex |
|- x e. _V |
| 12 |
|
df-bigcup |
|- Bigcup = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) ) |
| 13 |
|
brxp |
|- ( x ( _V X. _V ) B <-> ( x e. _V /\ B e. _V ) ) |
| 14 |
11 1 13
|
mpbir2an |
|- x ( _V X. _V ) B |
| 15 |
|
epel |
|- ( y _E z <-> y e. z ) |
| 16 |
15
|
rexbii |
|- ( E. z e. x y _E z <-> E. z e. x y e. z ) |
| 17 |
|
vex |
|- y e. _V |
| 18 |
17 11
|
coep |
|- ( y ( _E o. _E ) x <-> E. z e. x y _E z ) |
| 19 |
|
eluni2 |
|- ( y e. U. x <-> E. z e. x y e. z ) |
| 20 |
16 18 19
|
3bitr4ri |
|- ( y e. U. x <-> y ( _E o. _E ) x ) |
| 21 |
11 1 12 14 20
|
brtxpsd3 |
|- ( x Bigcup B <-> B = U. x ) |
| 22 |
|
eqcom |
|- ( B = U. x <-> U. x = B ) |
| 23 |
21 22
|
bitri |
|- ( x Bigcup B <-> U. x = B ) |
| 24 |
8 10 23
|
vtoclbg |
|- ( A e. _V -> ( A Bigcup B <-> U. A = B ) ) |
| 25 |
3 7 24
|
pm5.21nii |
|- ( A Bigcup B <-> U. A = B ) |