Theorem disj 4430

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2142, ax-11 2158, ax-12 2178. (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 3938	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2	1	eqeq1i 2741	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅)
3		dfcleq 2729	. . . . 5 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}))
4		df-clab 2715	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ [𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵))
5		sb6 2086	. . . . . . . 8 ⊢ ([𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ↔ ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
6		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
7		eleq1w 2818	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9		eleq1w 2818	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
10	9	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 → 𝑥 ∈ 𝐵))
11	8, 10	anim12d 609	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
12	6, 11	embantd 59	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ((𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
13	12	spimvw 1986	. . . . . . . . 9 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
14		eleq1a 2830	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐴))
15		eleq1a 2830	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐵))
16	14, 15	anim12ii 618	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
17	16	alrimiv 1927	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
18	13, 17	impbii 209	. . . . . . . 8 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
19	4, 5, 18	3bitri 297	. . . . . . 7 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	19	bibi2i 337	. . . . . 6 ⊢ ((𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
21	20	albii 1819	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
22	3, 21	bitri 275	. . . 4 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
23		eqcom 2743	. . . 4 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)})
24		bicom 222	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
25	24	albii 1819	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
26	22, 23, 25	3bitr4i 303	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
27		imnan 399	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
28		noel 4318	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
29	28	nbn 372	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
30	27, 29	bitr2i 276	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
31	30	albii 1819	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
32	2, 26, 31	3bitri 297	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
33		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
34	32, 33	bitr4i 278	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2714  ∀wral 3052   ∩ cin 3930  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-dif 3934  df-in 3938  df-nul 4314

This theorem is referenced by:  disjr  4431  disj1  4432  disjne  4435  disjord  5113  disjiund  5115  otiunsndisj  5500  dfpo2  6290  onxpdisj  6485  f0rn0  6768  onint  7789  zfreg  9614  kmlem4  10173  fin23lem30  10361  fin23lem31  10362  isf32lem3  10374  fpwwe2  10662  renfdisj  11300  fvinim0ffz  13807  s3iunsndisj  14992  metdsge  24794  ssltdisj  27790  dfpth2  29716  2wspmdisj  30323  subfacp1lem1  35206  disjabso  44967  dvmptfprodlem  45940  stoweidlem26  46022  stoweidlem59  46055  iundjiunlem  46455  otiunsndisjX  47275  upgrimpths  47889