Theorem ssdif0 4316

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 3909	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4300	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2113   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4283

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 2115  ax-9 2123  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-ss 3916  df-nul 4284

This theorem is referenced by:  difn0  4317  pssdifn0  4318  difidALT  4327  vdif0  4419  difrab0eq  4420  difin0  4424  symdifv  5039  frpoind  6298  ordintdif  6366  dffv2  6927  fndifnfp  7120  tfi  7793  peano5  7833  frrlem13  8238  frrlem14  8239  tz7.49  8374  oe0m1  8446  sdomdif  9051  sucdom2  9125  php3  9131  isinf  9163  unxpwdom2  9491  frind  9660  fin23lem26  10233  fin23lem21  10247  fin1a2lem13  10320  zornn0g  10413  fpwwe2lem12  10551  fpwwe2  10552  isumltss  15769  rpnnen2lem12  16148  chnccat  18547  symgsssg  19394  symgfisg  19395  psgnunilem5  19421  lspsnat  21098  lsppratlem6  21105  lspprat  21106  lbsextlem4  21114  cnsubrg  21380  opsrtoslem2  22009  psdmullem  22106  0ntr  23013  cmpfi  23350  dfconn2  23361  filconn  23825  cfinfil  23835  ufileu  23861  alexsublem  23986  ptcmplem2  23995  ptcmplem3  23996  restmetu  24512  reconnlem1  24769  bcthlem5  25282  itg10  25643  limcnlp  25833  noextendseq  27633  sltlpss  27880  upgrex  29114  uvtx01vtx  29419  ex-dif  30447  strlem1  32274  difininv  32541  eqdif  32543  difioo  32811  pmtrcnelor  33122  baselcarsg  34412  difelcarsg  34416  sibfof  34446  sitg0  34452  chtvalz  34735  onvf1odlem2  35247  onsucconni  36580  topdifinfeq  37494  nlpineqsn  37552  fdc  37885  setindtr  43208  oe0rif  43469  cantnfresb  43508  relnonrel  43770  inaex  44480  caragenunidm  46694