Step |
Hyp |
Ref |
Expression |
1 |
|
df-iun |
|- U_ x e. A B = { y | E. x e. A y e. B } |
2 |
1
|
sseq1i |
|- ( U_ x e. A B C_ C <-> { y | E. x e. A y e. B } C_ C ) |
3 |
|
abss |
|- ( { y | E. x e. A y e. B } C_ C <-> A. y ( E. x e. A y e. B -> y e. C ) ) |
4 |
|
dfss2 |
|- ( B C_ C <-> A. y ( y e. B -> y e. C ) ) |
5 |
4
|
ralbii |
|- ( A. x e. A B C_ C <-> A. x e. A A. y ( y e. B -> y e. C ) ) |
6 |
|
ralcom4 |
|- ( A. x e. A A. y ( y e. B -> y e. C ) <-> A. y A. x e. A ( y e. B -> y e. C ) ) |
7 |
|
r19.23v |
|- ( A. x e. A ( y e. B -> y e. C ) <-> ( E. x e. A y e. B -> y e. C ) ) |
8 |
7
|
albii |
|- ( A. y A. x e. A ( y e. B -> y e. C ) <-> A. y ( E. x e. A y e. B -> y e. C ) ) |
9 |
5 6 8
|
3bitrri |
|- ( A. y ( E. x e. A y e. B -> y e. C ) <-> A. x e. A B C_ C ) |
10 |
2 3 9
|
3bitri |
|- ( U_ x e. A B C_ C <-> A. x e. A B C_ C ) |