Theorem disjnf

Description: In case x is not free in B , disjointness is not so interesting since it reduces to cases where A is a singleton. (Google Groups discussion with Peter Mazsa.) (Contributed by Thierry Arnoux, 26-Jul-2018)

	Ref	Expression
Assertion	disjnf	|- ( Disj_ x e. A B <-> ( B = (/) \/ E* x x e. A ) )

Proof

Step	Hyp	Ref	Expression
1		inidm	|- ( B i^i B ) = B
2	1	eqeq1i	|- ( ( B i^i B ) = (/) <-> B = (/) )
3	2	orbi1i	|- ( ( ( B i^i B ) = (/) \/ A. x e. A A. y e. A x = y ) <-> ( B = (/) \/ A. x e. A A. y e. A x = y ) )
4		eqidd	|- ( x = y -> B = B )
5	4	disjor	|- ( Disj_ x e. A B <-> A. x e. A A. y e. A ( x = y \/ ( B i^i B ) = (/) ) )
6		orcom	|- ( ( x = y \/ ( B i^i B ) = (/) ) <-> ( ( B i^i B ) = (/) \/ x = y ) )
7	6	ralbii	|- ( A. y e. A ( x = y \/ ( B i^i B ) = (/) ) <-> A. y e. A ( ( B i^i B ) = (/) \/ x = y ) )
8		r19.32v	|- ( A. y e. A ( ( B i^i B ) = (/) \/ x = y ) <-> ( ( B i^i B ) = (/) \/ A. y e. A x = y ) )
9	7 8	bitri	|- ( A. y e. A ( x = y \/ ( B i^i B ) = (/) ) <-> ( ( B i^i B ) = (/) \/ A. y e. A x = y ) )
10	9	ralbii	|- ( A. x e. A A. y e. A ( x = y \/ ( B i^i B ) = (/) ) <-> A. x e. A ( ( B i^i B ) = (/) \/ A. y e. A x = y ) )
11		r19.32v	|- ( A. x e. A ( ( B i^i B ) = (/) \/ A. y e. A x = y ) <-> ( ( B i^i B ) = (/) \/ A. x e. A A. y e. A x = y ) )
12	5 10 11	3bitri	|- ( Disj_ x e. A B <-> ( ( B i^i B ) = (/) \/ A. x e. A A. y e. A x = y ) )
13		moel	|- ( E* x x e. A <-> A. x e. A A. y e. A x = y )
14	13	orbi2i	|- ( ( B = (/) \/ E* x x e. A ) <-> ( B = (/) \/ A. x e. A A. y e. A x = y ) )
15	3 12 14	3bitr4i	|- ( Disj_ x e. A B <-> ( B = (/) \/ E* x x e. A ) )