Step |
Hyp |
Ref |
Expression |
1 |
|
ssiun2sf.1 |
|- F/_ x A |
2 |
|
ssiun2sf.2 |
|- F/_ x C |
3 |
|
ssiun2sf.3 |
|- F/_ x D |
4 |
|
ssiun2sf.4 |
|- ( x = C -> B = D ) |
5 |
2 1
|
nfel |
|- F/ x C e. A |
6 |
|
nfiu1 |
|- F/_ x U_ x e. A B |
7 |
3 6
|
nfss |
|- F/ x D C_ U_ x e. A B |
8 |
5 7
|
nfim |
|- F/ x ( C e. A -> D C_ U_ x e. A B ) |
9 |
|
eleq1 |
|- ( x = C -> ( x e. A <-> C e. A ) ) |
10 |
4
|
sseq1d |
|- ( x = C -> ( B C_ U_ x e. A B <-> D C_ U_ x e. A B ) ) |
11 |
9 10
|
imbi12d |
|- ( x = C -> ( ( x e. A -> B C_ U_ x e. A B ) <-> ( C e. A -> D C_ U_ x e. A B ) ) ) |
12 |
|
ssiun2 |
|- ( x e. A -> B C_ U_ x e. A B ) |
13 |
2 8 11 12
|
vtoclgf |
|- ( C e. A -> ( C e. A -> D C_ U_ x e. A B ) ) |
14 |
13
|
pm2.43i |
|- ( C e. A -> D C_ U_ x e. A B ) |