Theorem reldisj 4453

Description: Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid ax-12 2177. (Revised by GG, 28-Jun-2024.)

Assertion

Ref	Expression
reldisj	⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))

Proof of Theorem reldisj

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ss 3968	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
2		eleq1w 2824	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
3		eleq1w 2824	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
4	2, 3	imbi12d 344	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ↔ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐶)))
5	4	spw 2033	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		pm5.44 542	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))))
7		eldif 3961	. . . . . . 7 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))
8	7	imbi2i 336	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)))
9	6, 8	bitr4di 289	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
10	5, 9	syl 17	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
11	1, 10	sylbi 217	. . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
12	11	albidv 1920	. 2 ⊢ (𝐴 ⊆ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
13		disj1 4452	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
14		df-ss 3968	. 2 ⊢ (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)))
15	12, 13, 14	3bitr4g 314	1 ⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ∖ cdif 3948   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333

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 2007  ax-8 2110  ax-9 2118  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 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968  df-nul 4334

This theorem is referenced by:  disj2  4458  ssdifsn  4788  oacomf1olem  8602  domdifsn  9094  elfiun  9470  cantnfp1lem3  9720  ssxr  11330  structcnvcnv  17190  fidomndrng  20774  elcls  23081  ist1-2  23355  nrmsep2  23364  nrmsep  23365  isnrm3  23367  isreg2  23385  hauscmplem  23414  connsub  23429  iunconnlem  23435  llycmpkgen2  23558  hausdiag  23653  trfil3  23896  isufil2  23916  filufint  23928  blcld  24518  i1fima2  25714  i1fd  25716  nbgrssvwo2  29379  pliguhgr  30505  symgcom2  33104  ssdifidlprm  33486  inunissunidif  37376  poimirlem15  37642  itg2addnclem2  37679  ntrk0kbimka  44052  ntrneicls11  44103  gneispace  44147  opndisj  48800  seposep  48823