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 Gino Giotto, 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 ) = { z | ( z e. A /\ z e. B ) }
2	1	eqeq1i	|- ( ( A i^i B ) = (/) <-> { z | ( z e. A /\ z e. B ) } = (/) )
3		dfcleq	|- ( (/) = { z | ( z e. A /\ z e. B ) } <-> A. x ( x e. (/) <-> x e. { z | ( z e. A /\ z e. B ) } ) )
4		df-clab	|- ( x e. { z | ( z e. A /\ z e. B ) } <-> [ x / z ] ( z e. A /\ z e. B ) )
5		sb6	|- ( [ x / z ] ( z e. A /\ z e. B ) <-> A. z ( z = x -> ( z e. A /\ z e. B ) ) )
6		id	|- ( z = x -> z = x )
7		eleq1w	|- ( z = x -> ( z e. A <-> x e. A ) )
8	7	biimpd	|- ( z = x -> ( z e. A -> x e. A ) )
9		eleq1w	|- ( z = x -> ( z e. B <-> x e. B ) )
10	9	biimpd	|- ( z = x -> ( z e. B -> x e. B ) )
11	8 10	anim12d	|- ( z = x -> ( ( z e. A /\ z e. B ) -> ( x e. A /\ x e. B ) ) )
12	6 11	embantd	|- ( z = x -> ( ( z = x -> ( z e. A /\ z e. B ) ) -> ( x e. A /\ x e. B ) ) )
13	12	spimvw	|- ( A. z ( z = x -> ( z e. A /\ z e. B ) ) -> ( x e. A /\ x e. B ) )
14		eleq1a	|- ( x e. A -> ( z = x -> z e. A ) )
15		eleq1a	|- ( x e. B -> ( z = x -> z e. B ) )
16	14 15	anim12ii	|- ( ( x e. A /\ x e. B ) -> ( z = x -> ( z e. A /\ z e. B ) ) )
17	16	alrimiv	|- ( ( x e. A /\ x e. B ) -> A. z ( z = x -> ( z e. A /\ z e. B ) ) )
18	13 17	impbii	|- ( A. z ( z = x -> ( z e. A /\ z e. B ) ) <-> ( x e. A /\ x e. B ) )
19	4 5 18	3bitri	|- ( x e. { z | ( z e. A /\ z e. B ) } <-> ( x e. A /\ x e. B ) )
20	19	bibi2i	|- ( ( x e. (/) <-> x e. { z | ( z e. A /\ z e. B ) } ) <-> ( x e. (/) <-> ( x e. A /\ x e. B ) ) )
21	20	albii	|- ( A. x ( x e. (/) <-> x e. { z | ( z e. A /\ z e. B ) } ) <-> A. x ( x e. (/) <-> ( x e. A /\ x e. B ) ) )
22	3 21	bitri	|- ( (/) = { z | ( z e. A /\ z e. B ) } <-> A. x ( x e. (/) <-> ( x e. A /\ x e. B ) ) )
23		eqcom	|- ( { z | ( z e. A /\ z e. B ) } = (/) <-> (/) = { z | ( z e. A /\ z e. B ) } )
24		bicom	|- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. (/) <-> ( x e. A /\ x e. B ) ) )
25	24	albii	|- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. (/) <-> ( x e. A /\ x e. B ) ) )
26	22 23 25	3bitr4i	|- ( { z | ( z e. A /\ z e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
27		imnan	|- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
28		noel	|- -. x e. (/)
29	28	nbn	|- ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
30	27 29	bitr2i	|- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
31	30	albii	|- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
32	2 26 31	3bitri	|- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
33		df-ral	|- ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
34	32 33	bitr4i	|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )