Step |
Hyp |
Ref |
Expression |
1 |
|
disjiunel.1 |
|- ( ph -> Disj_ x e. A B ) |
2 |
|
disjiunel.2 |
|- ( x = Y -> B = D ) |
3 |
|
disjiunel.3 |
|- ( ph -> E C_ A ) |
4 |
|
disjiunel.4 |
|- ( ph -> Y e. ( A \ E ) ) |
5 |
4
|
eldifad |
|- ( ph -> Y e. A ) |
6 |
5
|
snssd |
|- ( ph -> { Y } C_ A ) |
7 |
3 6
|
unssd |
|- ( ph -> ( E u. { Y } ) C_ A ) |
8 |
|
disjss1 |
|- ( ( E u. { Y } ) C_ A -> ( Disj_ x e. A B -> Disj_ x e. ( E u. { Y } ) B ) ) |
9 |
7 1 8
|
sylc |
|- ( ph -> Disj_ x e. ( E u. { Y } ) B ) |
10 |
4
|
eldifbd |
|- ( ph -> -. Y e. E ) |
11 |
2
|
disjunsn |
|- ( ( Y e. A /\ -. Y e. E ) -> ( Disj_ x e. ( E u. { Y } ) B <-> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) ) ) |
12 |
5 10 11
|
syl2anc |
|- ( ph -> ( Disj_ x e. ( E u. { Y } ) B <-> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) ) ) |
13 |
9 12
|
mpbid |
|- ( ph -> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) ) |
14 |
13
|
simprd |
|- ( ph -> ( U_ x e. E B i^i D ) = (/) ) |