Metamath Proof Explorer


Theorem disjiunel

Description: A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020)

Ref Expression
Hypotheses disjiunel.1 φ Disj x A B
disjiunel.2 x = Y B = D
disjiunel.3 φ E A
disjiunel.4 φ Y A E
Assertion disjiunel φ x E B D =

Proof

Step Hyp Ref Expression
1 disjiunel.1 φ Disj x A B
2 disjiunel.2 x = Y B = D
3 disjiunel.3 φ E A
4 disjiunel.4 φ Y A E
5 4 eldifad φ Y A
6 5 snssd φ Y A
7 3 6 unssd φ E Y A
8 disjss1 E Y A Disj x A B Disj x E Y B
9 7 1 8 sylc φ Disj x E Y B
10 4 eldifbd φ ¬ Y E
11 2 disjunsn Y A ¬ Y E Disj x E Y B Disj x E B x E B D =
12 5 10 11 syl2anc φ Disj x E Y B Disj x E B x E B D =
13 9 12 mpbid φ Disj x E B x E B D =
14 13 simprd φ x E B D =