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 ) =/= (/) ) )