Theorem reldisj 4450

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 2169. (Revised by Gino Giotto, 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		dfss2 3967	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
2		eleq1w 2814	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
3		eleq1w 2814	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
4	2, 3	imbi12d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ↔ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐶)))
5	4	spw 2035	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		pm5.44 541	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))))
7		eldif 3957	. . . . . . 7 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))
8	7	imbi2i 335	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)))
9	6, 8	bitr4di 288	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
10	5, 9	syl 17	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
11	1, 10	sylbi 216	. . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
12	11	albidv 1921	. 2 ⊢ (𝐴 ⊆ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
13		disj1 4449	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
14		dfss2 3967	. 2 ⊢ (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)))
15	12, 13, 14	3bitr4g 313	1 ⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1537   = wceq 1539   ∈ wcel 2104   ∖ cdif 3944   ∩ cin 3946   ⊆ wss 3947  ∅c0 4321

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-v 3474  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  disj2  4456  ssdifsn  4790  oacomf1olem  8566  domdifsn  9056  elfiun  9427  cantnfp1lem3  9677  ssxr  11287  structcnvcnv  17090  fidomndrng  21126  elcls  22797  ist1-2  23071  nrmsep2  23080  nrmsep  23081  isnrm3  23083  isreg2  23101  hauscmplem  23130  connsub  23145  iunconnlem  23151  llycmpkgen2  23274  hausdiag  23369  trfil3  23612  isufil2  23632  filufint  23644  blcld  24234  i1fima2  25428  i1fd  25430  nbgrssvwo2  28886  pliguhgr  30006  symgcom2  32515  inunissunidif  36559  poimirlem15  36806  itg2addnclem2  36843  ntrk0kbimka  43092  ntrneicls11  43143  gneispace  43187  opndisj  47622  seposep  47645