Theorem ssdif0 4313

Description: Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
ssdif0	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Proof of Theorem ssdif0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iman 401	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3907	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3914	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4297	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2111   ∖ cdif 3894   ⊆ wss 3897  ∅c0 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-ss 3914  df-nul 4281

This theorem is referenced by:  difn0  4314  pssdifn0  4315  difidALT  4324  vdif0  4416  difrab0eq  4417  difin0  4421  symdifv  5032  frpoind  6289  ordintdif  6357  dffv2  6917  fndifnfp  7110  tfi  7783  peano5  7823  frrlem13  8228  frrlem14  8229  tz7.49  8364  oe0m1  8436  sdomdif  9038  sucdom2  9112  php3  9118  isinf  9149  unxpwdom2  9474  frind  9643  fin23lem26  10216  fin23lem21  10230  fin1a2lem13  10303  zornn0g  10396  fpwwe2lem12  10533  fpwwe2  10534  isumltss  15755  rpnnen2lem12  16134  chnccat  18532  symgsssg  19379  symgfisg  19380  psgnunilem5  19406  lspsnat  21082  lsppratlem6  21089  lspprat  21090  lbsextlem4  21098  cnsubrg  21364  opsrtoslem2  21991  psdmullem  22080  0ntr  22986  cmpfi  23323  dfconn2  23334  filconn  23798  cfinfil  23808  ufileu  23834  alexsublem  23959  ptcmplem2  23968  ptcmplem3  23969  restmetu  24485  reconnlem1  24742  bcthlem5  25255  itg10  25616  limcnlp  25806  noextendseq  27606  sltlpss  27853  upgrex  29070  uvtx01vtx  29375  ex-dif  30403  strlem1  32230  difininv  32497  eqdif  32499  difioo  32765  pmtrcnelor  33060  baselcarsg  34319  difelcarsg  34323  sibfof  34353  sitg0  34359  chtvalz  34642  onvf1odlem2  35148  onsucconni  36479  topdifinfeq  37392  nlpineqsn  37450  fdc  37793  setindtr  43065  oe0rif  43326  cantnfresb  43365  relnonrel  43628  inaex  44338  caragenunidm  46554