Metamath Proof Explorer


Theorem ndisj2

Description: A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis ndisj2.1 x = y B = C
Assertion ndisj2 ¬ Disj x A B x A y A x y B C

Proof

Step Hyp Ref Expression
1 ndisj2.1 x = y B = C
2 1 disjor Disj x A B x A y A x = y B C =
3 2 notbii ¬ Disj x A B ¬ x A y A x = y B C =
4 rexnal x A ¬ y A x = y B C = ¬ x A y A x = y B C =
5 rexnal y A ¬ x = y B C = ¬ y A x = y B C =
6 ioran ¬ x = y B C = ¬ x = y ¬ B C =
7 df-ne x y ¬ x = y
8 df-ne B C ¬ B C =
9 7 8 anbi12i x y B C ¬ x = y ¬ B C =
10 6 9 bitr4i ¬ x = y B C = x y B C
11 10 rexbii y A ¬ x = y B C = y A x y B C
12 5 11 bitr3i ¬ y A x = y B C = y A x y B C
13 12 rexbii x A ¬ y A x = y B C = x A y A x y B C
14 3 4 13 3bitr2i ¬ Disj x A B x A y A x y B C