Theorem ssdif0 3896

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 439	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3550	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 324	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1737	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3557	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 3888	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 291	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875

This theorem is referenced by:  difn0  3897  pssdifn0  3898  difid  3902  vdif0  3989  difrab0eq  3990  difin0  3993  symdifv  4534  wfi  5630  ordintdif  5691  dffv2  6181  fndifnfp  6347  tfi  6945  peano5  6981  wfrlem8  7309  wfrlem16  7317  tz7.49  7427  oe0m1  7488  sdomdif  7993  php3  8031  sucdom2  8041  isinf  8058  unxpwdom2  8376  fin23lem26  9030  fin23lem21  9044  fin1a2lem13  9117  zornn0g  9210  fpwwe2lem13  9343  fpwwe2  9344  isumltss  14419  rpnnen2lem12  14793  symgsssg  17710  symgfisg  17711  psgnunilem5  17737  lspsnat  18966  lsppratlem6  18973  lspprat  18974  lbsextlem4  18982  opsrtoslem2  19306  cnsubrg  19625  0ntr  20685  cmpfi  21021  dfcon2  21032  filcon  21497  cfinfil  21507  ufileu  21533  alexsublem  21658  ptcmplem2  21667  ptcmplem3  21668  restmetu  22185  reconnlem1  22437  bcthlem5  22933  itg10  23261  limcnlp  23448  upgrex  25759  umgraex  25852  uvtx01vtx  26020  ex-dif  26672  strlem1  28493  difioo  28934  baselcarsg  29695  difelcarsg  29699  sibfof  29729  sitg0  29735  frind  30984  onsucconi  31606  topdifinfeq  32374  fdc  32711  setindtr  36609  relnonrel  36912  caragenunidm  39398  uvtxa01vtx0  40623