Theorem disj 4345

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2143, ax-11 2159, ax-12 2176. (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 3866	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2	1	eqeq1i 2764	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅)
3		dfcleq 2752	. . . . 5 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}))
4		df-clab 2737	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ [𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵))
5		sb6 2091	. . . . . . . 8 ⊢ ([𝑥 / 𝑧](𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) ↔ ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
6		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
7		eleq1w 2835	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴))
8	7	biimpd 232	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 → 𝑥 ∈ 𝐴))
9		eleq1w 2835	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵))
10	9	biimpd 232	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐵 → 𝑥 ∈ 𝐵))
11	8, 10	anim12d 612	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
12	6, 11	embantd 59	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ((𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
13	12	spimvw 2003	. . . . . . . . 9 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
14		eleq1a 2848	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐴))
15		eleq1a 2848	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (𝑧 = 𝑥 → 𝑧 ∈ 𝐵))
16	14, 15	anim12ii 621	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
17	16	alrimiv 1929	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → ∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)))
18	13, 17	impbii 212	. . . . . . . 8 ⊢ (∀𝑧(𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
19	4, 5, 18	3bitri 301	. . . . . . 7 ⊢ (𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
20	19	bibi2i 342	. . . . . 6 ⊢ ((𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
21	20	albii 1822	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
22	3, 21	bitri 278	. . . 4 ⊢ (∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
23		eqcom 2766	. . . 4 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∅ = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)})
24		bicom 225	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
25	24	albii 1822	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
26	22, 23, 25	3bitr4i 307	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
27		imnan 404	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
28		noel 4231	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
29	28	nbn 377	. . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅))
30	27, 29	bitr2i 279	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
31	30	albii 1822	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
32	2, 26, 31	3bitri 301	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
33		df-ral 3076	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
34	32, 33	bitr4i 281	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1537   = wceq 1539  [wsb 2070   ∈ wcel 2112  {cab 2736  ∀wral 3071   ∩ cin 3858  ∅c0 4226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ral 3076  df-dif 3862  df-in 3866  df-nul 4227

This theorem is referenced by:  disjr  4347  disj1  4348  disjne  4352  disjord  5021  disjiund  5023  otiunsndisj  5380  onxpdisj  6290  f0rn0  6550  onint  7510  zfreg  9085  kmlem4  9606  fin23lem30  9795  fin23lem31  9796  isf32lem3  9808  fpwwe2  10096  renfdisj  10732  fvinim0ffz  13198  s3iunsndisj  14368  metdsge  23543  2wspmdisj  28214  subfacp1lem1  32650  dfpo2  33231  dvmptfprodlem  42945  stoweidlem26  43027  stoweidlem59  43060  iundjiunlem  43457  otiunsndisjX  44196