Theorem disj 4403

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 3912	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2	1	eqeq1i 2734	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅)
3		dfcleq 2722	. . . . 5 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}))
4		df-clab 2708	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ [𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵))
5		sb6 2086	. . . . . . . 8 ⊢ ([𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ↔ ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
6		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
7		eleq1w 2811	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9		eleq1w 2811	. . . . . . . . . . . . 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 2823	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐴))
15		eleq1a 2823	. . . . . . . . . . 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 2736	. . . 4 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)})
24		bicom 222	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
25	24	albii 1819	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
26	22, 23, 25	3bitr4i 303	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
27		imnan 399	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
28		noel 4291	. . . . . 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 3045	. 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 2707  ∀wral 3044   ∩ cin 3904  ∅c0 4286

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-dif 3908  df-in 3912  df-nul 4287

This theorem is referenced by:  disjr  4404  disj1  4405  disjne  4408  disjord  5084  disjiund  5086  otiunsndisj  5467  dfpo2  6248  onxpdisj  6438  f0rn0  6713  onint  7730  zfreg  9507  kmlem4  10067  fin23lem30  10255  fin23lem31  10256  isf32lem3  10268  fpwwe2  10556  renfdisj  11194  fvinim0ffz  13707  s3iunsndisj  14893  metdsge  24754  ssltdisj  27752  dfpth2  29692  2wspmdisj  30299  subfacp1lem1  35151  disjabso  44949  dvmptfprodlem  45926  stoweidlem26  46008  stoweidlem59  46041  iundjiunlem  46441  otiunsndisjX  47264  upgrimpths  47894