Theorem ssdif0 4252

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 405	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3853	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 338	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1826	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3863	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4232	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ∖ cdif 3840   ⊆ wss 3843  ∅c0 4211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-in 3850  df-ss 3860  df-nul 4212

This theorem is referenced by:  difn0  4253  pssdifn0  4254  difidALT  4260  vdif0  4358  difrab0eq  4359  difin0  4363  symdifv  4971  wfi  6162  ordintdif  6221  dffv2  6765  fndifnfp  6950  tfi  7589  peano5  7626  peano5OLD  7627  wfrlem8  7993  wfrlem16  8001  tz7.49  8112  oe0m1  8179  sucdom2  8678  sdomdif  8717  php3  8755  isinf  8812  unxpwdom2  9127  fin23lem26  9827  fin23lem21  9841  fin1a2lem13  9914  zornn0g  10007  fpwwe2lem12  10144  fpwwe2  10145  isumltss  15298  rpnnen2lem12  15672  symgsssg  18715  symgfisg  18716  psgnunilem5  18742  lspsnat  20038  lsppratlem6  20045  lspprat  20046  lbsextlem4  20054  cnsubrg  20279  opsrtoslem2  20869  0ntr  21824  cmpfi  22161  dfconn2  22172  filconn  22636  cfinfil  22646  ufileu  22672  alexsublem  22797  ptcmplem2  22806  ptcmplem3  22807  restmetu  23325  reconnlem1  23580  bcthlem5  24082  itg10  24442  limcnlp  24632  upgrex  27039  uvtx01vtx  27341  ex-dif  28362  strlem1  30187  difininv  30440  eqdif  30442  difioo  30680  pmtrcnelor  30939  baselcarsg  31845  difelcarsg  31849  sibfof  31879  sitg0  31885  chtvalz  32181  frpoind  33387  frind  33395  frrlem13  33457  frrlem14  33458  noextendseq  33515  sltlpss  33732  onsucconni  34271  topdifinfeq  35166  nlpineqsn  35224  fdc  35548  setindtr  40440  relnonrel  40762  inaex  41479  caragenunidm  43610