Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( A e. U_ x e. B C -> A e. _V ) |
2 |
|
elex |
|- ( A e. C -> A e. _V ) |
3 |
2
|
rexlimivw |
|- ( E. x e. B A e. C -> A e. _V ) |
4 |
|
eleq1 |
|- ( y = w -> ( y e. C <-> w e. C ) ) |
5 |
4
|
rexbidv |
|- ( y = w -> ( E. x e. B y e. C <-> E. x e. B w e. C ) ) |
6 |
|
eleq1 |
|- ( w = A -> ( w e. C <-> A e. C ) ) |
7 |
6
|
rexbidv |
|- ( w = A -> ( E. x e. B w e. C <-> E. x e. B A e. C ) ) |
8 |
|
df-iun |
|- U_ x e. B C = { y | E. x e. B y e. C } |
9 |
5 7 8
|
elab2gw |
|- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) ) |
10 |
1 3 9
|
pm5.21nii |
|- ( A e. U_ x e. B C <-> E. x e. B A e. C ) |