Theorem disj 4456

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 2155, ax-12 2175. (Revised by GG, 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 3970	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2	1	eqeq1i 2740	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅)
3		dfcleq 2728	. . . . 5 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}))
4		df-clab 2713	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ [𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵))
5		sb6 2083	. . . . . . . 8 ⊢ ([𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ↔ ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
6		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
7		eleq1w 2822	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9		eleq1w 2822	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
10	9	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 → 𝑥 ∈ 𝐵))
11	8, 10	anim12d 609	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
12	6, 11	embantd 59	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ((𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
13	12	spimvw 1993	. . . . . . . . 9 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
14		eleq1a 2834	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐴))
15		eleq1a 2834	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐵))
16	14, 15	anim12ii 618	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
17	16	alrimiv 1925	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
18	13, 17	impbii 209	. . . . . . . 8 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
19	4, 5, 18	3bitri 297	. . . . . . 7 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	19	bibi2i 337	. . . . . 6 ⊢ ((𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
21	20	albii 1816	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
22	3, 21	bitri 275	. . . 4 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
23		eqcom 2742	. . . 4 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)})
24		bicom 222	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
25	24	albii 1816	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
26	22, 23, 25	3bitr4i 303	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
27		imnan 399	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
28		noel 4344	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
29	28	nbn 372	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
30	27, 29	bitr2i 276	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
31	30	albii 1816	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
32	2, 26, 31	3bitri 297	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
33		df-ral 3060	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
34	32, 33	bitr4i 278	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  [wsb 2062   ∈ wcel 2106  {cab 2712  ∀wral 3059   ∩ cin 3962  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-dif 3966  df-in 3970  df-nul 4340

This theorem is referenced by:  disjr  4457  disj1  4458  disjne  4461  disjord  5137  disjiund  5139  otiunsndisj  5530  dfpo2  6318  onxpdisj  6512  f0rn0  6794  onint  7810  zfreg  9633  kmlem4  10192  fin23lem30  10380  fin23lem31  10381  isf32lem3  10393  fpwwe2  10681  renfdisj  11319  fvinim0ffz  13822  s3iunsndisj  15004  metdsge  24885  ssltdisj  27881  2wspmdisj  30366  subfacp1lem1  35164  dvmptfprodlem  45900  stoweidlem26  45982  stoweidlem59  46015  iundjiunlem  46415  otiunsndisjX  47229