Theorem ssdif0 4320

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ∖ cdif 3900   ⊆ wss 3903  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920  df-nul 4288

This theorem is referenced by:  difn0  4321  pssdifn0  4322  difidALT  4331  vdif0  4423  difrab0eq  4424  difin0  4428  symdifv  5043  frpoind  6308  ordintdif  6376  dffv2  6937  fndifnfp  7132  tfi  7805  peano5  7845  frrlem13  8250  frrlem14  8251  tz7.49  8386  oe0m1  8458  sdomdif  9065  sucdom2  9139  php3  9145  isinf  9177  unxpwdom2  9505  frind  9674  fin23lem26  10247  fin23lem21  10261  fin1a2lem13  10334  zornn0g  10427  fpwwe2lem12  10565  fpwwe2  10566  isumltss  15783  rpnnen2lem12  16162  chnccat  18561  symgsssg  19408  symgfisg  19409  psgnunilem5  19435  lspsnat  21112  lsppratlem6  21119  lspprat  21120  lbsextlem4  21128  cnsubrg  21394  opsrtoslem2  22023  psdmullem  22120  0ntr  23027  cmpfi  23364  dfconn2  23375  filconn  23839  cfinfil  23849  ufileu  23875  alexsublem  24000  ptcmplem2  24009  ptcmplem3  24010  restmetu  24526  reconnlem1  24783  bcthlem5  25296  itg10  25657  limcnlp  25847  noextendseq  27647  ltslpss  27916  upgrex  29177  uvtx01vtx  29482  ex-dif  30510  strlem1  32338  difininv  32604  eqdif  32606  difioo  32873  pmtrcnelor  33185  baselcarsg  34484  difelcarsg  34488  sibfof  34518  sitg0  34524  chtvalz  34807  onvf1odlem2  35320  onsucconni  36653  topdifinfeq  37605  nlpineqsn  37663  fdc  37996  setindtr  43381  oe0rif  43642  cantnfresb  43681  relnonrel  43943  inaex  44653  caragenunidm  46866