Theorem disj

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004) Avoid ax-10 , ax-11 , ax-12 . (Revised by GG, 28-Jun-2024)

	Ref	Expression
Assertion	disj	|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Proof

Step	Hyp	Ref	Expression
1		df-in	|- ( A i^i B ) = { y | ( y e. A /\ y e. B ) }
2	1	eqeq1i	|- ( ( A i^i B ) = (/) <-> { y | ( y e. A /\ y e. B ) } = (/) )
3		eleq1w	|- ( y = x -> ( y e. A <-> x e. A ) )
4		eleq1w	|- ( y = x -> ( y e. B <-> x e. B ) )
5	3 4	anbi12d	|- ( y = x -> ( ( y e. A /\ y e. B ) <-> ( x e. A /\ x e. B ) ) )
6	5	eqabcbw	|- ( { y | ( y e. A /\ y e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
7		imnan	|- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
8		noel	|- -. x e. (/)
9	8	nbn	|- ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
10	7 9	bitr2i	|- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
11	10	albii	|- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
12	2 6 11	3bitri	|- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
13		df-ral	|- ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
14	12 13	bitr4i	|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )