Theorem reldisj 4405

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 2212. (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 3896	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
2		eleq1w 2843	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
3		eleq1w 2843	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶))
4	2, 3	imbi12d 347	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ↔ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐶)))
5	4	spw 2066	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		pm5.44 552	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))))
7		eldif 4049	. . . . . . 7 ⊢ (𝑥 ∈ (𝐶 ∖ 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵))
8	7	imbi2i 339	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐵)))
9	6, 8	bitr4di 292	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
10	5, 9	syl 18	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
11	1, 10	sylbi 220	. . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
12	11	albidv 1952	. 2 ⊢ (𝐴 ⊆ 𝐶 → (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵))))
13		disj1 4404	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
14		df-ss 3896	. 2 ⊢ (𝐴 ⊆ (𝐶 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐶 ∖ 𝐵)))
15	12, 13, 14	3bitr4g 317	1 ⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-nul 4279

This theorem is used by:  disj2  4410  ssdifsn  4747  oacomf1olem  8575  domdifsn  9082  elfiun  9425  cantnfp1lem3  9684  ssxr  11382  structcnvcnv  17336  fidomndrng  21036  ssdifidlprm  21647  elcls  23396  ist1-2  23670  nrmsep2  23679  nrmsep  23680  isnrm3  23682  isreg2  23700  hauscmplem  23729  connsub  23744  iunconnlem  23750  llycmpkgen2  23874  hausdiag  23969  trfil3  24212  isufil2  24232  filufint  24244  blcld  24829  i1fima2  26005  i1fd  26007  nbgrssvwo2  29948  pliguhgr  31093  symgcom2  33691  inunissunidif  38391  poimirlem15  38646  itg2addnclem2  38683  ntrk0kbimka  45132  ntrneicls11  45183  gneispace  45227  opndisj  50110  seposep  50133