Metamath Proof Explorer


Theorem ndisj2

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

Ref Expression
Hypothesis ndisj2.1 x=yB=C
Assertion ndisj2 ¬DisjxABxAyAxyBC

Proof

Step Hyp Ref Expression
1 ndisj2.1 x=yB=C
2 1 disjor DisjxABxAyAx=yBC=
3 2 notbii ¬DisjxAB¬xAyAx=yBC=
4 rexnal xA¬yAx=yBC=¬xAyAx=yBC=
5 rexnal yA¬x=yBC=¬yAx=yBC=
6 ioran ¬x=yBC=¬x=y¬BC=
7 df-ne xy¬x=y
8 df-ne BC¬BC=
9 7 8 anbi12i xyBC¬x=y¬BC=
10 6 9 bitr4i ¬x=yBC=xyBC
11 10 rexbii yA¬x=yBC=yAxyBC
12 5 11 bitr3i ¬yAx=yBC=yAxyBC
13 12 rexbii xA¬yAx=yBC=xAyAxyBC
14 3 4 13 3bitr2i ¬DisjxABxAyAxyBC