This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. A B <-> E. x e. A E. y e. A ( x =/= y /\ ( B i^i C ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 ndisj2.1 
 |-  ( x = y -> B = C )
2 1 disjor 
 |-  ( Disj_ x e. A B <-> A. x e. A A. y e. A ( x = y \/ ( B i^i C ) = (/) ) )
3 2 notbii 
 |-  ( -. Disj_ x e. A B <-> -. A. x e. A A. y e. A ( x = y \/ ( B i^i C ) = (/) ) )
4 rexnal 
 |-  ( E. x e. A -. A. y e. A ( x = y \/ ( B i^i C ) = (/) ) <-> -. A. x e. A A. y e. A ( x = y \/ ( B i^i C ) = (/) ) )
5 rexnal 
 |-  ( E. y e. A -. ( x = y \/ ( B i^i C ) = (/) ) <-> -. A. y e. A ( x = y \/ ( B i^i C ) = (/) ) )
6 ioran 
 |-  ( -. ( x = y \/ ( B i^i C ) = (/) ) <-> ( -. x = y /\ -. ( B i^i C ) = (/) ) )
7 df-ne 
 |-  ( x =/= y <-> -. x = y )
8 df-ne 
 |-  ( ( B i^i C ) =/= (/) <-> -. ( B i^i C ) = (/) )
9 7 8 anbi12i 
 |-  ( ( x =/= y /\ ( B i^i C ) =/= (/) ) <-> ( -. x = y /\ -. ( B i^i C ) = (/) ) )
10 6 9 bitr4i 
 |-  ( -. ( x = y \/ ( B i^i C ) = (/) ) <-> ( x =/= y /\ ( B i^i C ) =/= (/) ) )
11 10 rexbii 
 |-  ( E. y e. A -. ( x = y \/ ( B i^i C ) = (/) ) <-> E. y e. A ( x =/= y /\ ( B i^i C ) =/= (/) ) )
12 5 11 bitr3i 
 |-  ( -. A. y e. A ( x = y \/ ( B i^i C ) = (/) ) <-> E. y e. A ( x =/= y /\ ( B i^i C ) =/= (/) ) )
13 12 rexbii 
 |-  ( E. x e. A -. A. y e. A ( x = y \/ ( B i^i C ) = (/) ) <-> E. x e. A E. y e. A ( x =/= y /\ ( B i^i C ) =/= (/) ) )
14 3 4 13 3bitr2i 
 |-  ( -. Disj_ x e. A B <-> E. x e. A E. y e. A ( x =/= y /\ ( B i^i C ) =/= (/) ) )