Theorem ssdif0 4389

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537   ∈ wcel 2108   ∖ cdif 3973   ⊆ wss 3976  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993  df-nul 4353

This theorem is referenced by:  difn0  4390  pssdifn0  4391  difidALT  4399  vdif0  4492  difrab0eq  4493  difin0  4497  symdifv  5109  frpoind  6374  wfiOLD  6383  ordintdif  6445  dffv2  7017  fndifnfp  7210  tfi  7890  peano5  7932  peano5OLD  7933  frrlem13  8339  frrlem14  8340  wfrlem8OLD  8372  wfrlem16OLD  8380  tz7.49  8501  oe0m1  8577  sucdom2OLD  9148  sdomdif  9191  sucdom2  9269  php3  9275  php3OLD  9287  isinf  9323  isinfOLD  9324  unxpwdom2  9657  frind  9819  fin23lem26  10394  fin23lem21  10408  fin1a2lem13  10481  zornn0g  10574  fpwwe2lem12  10711  fpwwe2  10712  isumltss  15896  rpnnen2lem12  16273  symgsssg  19509  symgfisg  19510  psgnunilem5  19536  lspsnat  21170  lsppratlem6  21177  lspprat  21178  lbsextlem4  21186  cnsubrg  21468  opsrtoslem2  22103  psdmullem  22192  0ntr  23100  cmpfi  23437  dfconn2  23448  filconn  23912  cfinfil  23922  ufileu  23948  alexsublem  24073  ptcmplem2  24082  ptcmplem3  24083  restmetu  24604  reconnlem1  24867  bcthlem5  25381  itg10  25742  limcnlp  25933  noextendseq  27730  sltlpss  27963  upgrex  29127  uvtx01vtx  29432  ex-dif  30455  strlem1  32282  difininv  32547  eqdif  32549  difioo  32787  pmtrcnelor  33084  baselcarsg  34271  difelcarsg  34275  sibfof  34305  sitg0  34311  chtvalz  34606  onsucconni  36403  topdifinfeq  37316  nlpineqsn  37374  fdc  37705  setindtr  42981  oe0rif  43247  cantnfresb  43286  relnonrel  43549  inaex  44266  caragenunidm  46429