Theorem disj 4378

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

Assertion

Ref	Expression
disj	⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem disj

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-in 3890	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2	1	eqeq1i 2743	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅)
3		dfcleq 2731	. . . . 5 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}))
4		df-clab 2716	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ [𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵))
5		sb6 2089	. . . . . . . 8 ⊢ ([𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ↔ ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
6		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
7		eleq1w 2821	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 228	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9		eleq1w 2821	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
10	9	biimpd 228	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 → 𝑥 ∈ 𝐵))
11	8, 10	anim12d 608	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
12	6, 11	embantd 59	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ((𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
13	12	spimvw 2000	. . . . . . . . 9 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
14		eleq1a 2834	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐴))
15		eleq1a 2834	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐵))
16	14, 15	anim12ii 617	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
17	16	alrimiv 1931	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
18	13, 17	impbii 208	. . . . . . . 8 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
19	4, 5, 18	3bitri 296	. . . . . . 7 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	19	bibi2i 337	. . . . . 6 ⊢ ((𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
21	20	albii 1823	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
22	3, 21	bitri 274	. . . 4 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
23		eqcom 2745	. . . 4 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)})
24		bicom 221	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
25	24	albii 1823	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
26	22, 23, 25	3bitr4i 302	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
27		imnan 399	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
28		noel 4261	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
29	28	nbn 372	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
30	27, 29	bitr2i 275	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
31	30	albii 1823	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
32	2, 26, 31	3bitri 296	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
33		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
34	32, 33	bitr4i 277	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539  [wsb 2068   ∈ wcel 2108  {cab 2715  ∀wral 3063   ∩ cin 3882  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-dif 3886  df-in 3890  df-nul 4254

This theorem is referenced by:  disjr  4380  disj1  4381  disjne  4385  disjord  5058  disjiund  5060  otiunsndisj  5428  dfpo2  6188  onxpdisj  6371  f0rn0  6643  onint  7617  zfreg  9284  kmlem4  9840  fin23lem30  10029  fin23lem31  10030  isf32lem3  10042  fpwwe2  10330  renfdisj  10966  fvinim0ffz  13434  s3iunsndisj  14607  metdsge  23918  2wspmdisj  28602  subfacp1lem1  33041  ssltdisj  33942  dvmptfprodlem  43375  stoweidlem26  43457  stoweidlem59  43490  iundjiunlem  43887  otiunsndisjX  44658