Theorem ssdif0 4341

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ∖ cdif 3923   ⊆ wss 3926  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943  df-nul 4309

This theorem is referenced by:  difn0  4342  pssdifn0  4343  difidALT  4352  vdif0  4444  difrab0eq  4445  difin0  4449  symdifv  5062  frpoind  6331  wfiOLD  6340  ordintdif  6403  dffv2  6974  fndifnfp  7168  tfi  7848  peano5  7889  frrlem13  8297  frrlem14  8298  wfrlem8OLD  8330  wfrlem16OLD  8338  tz7.49  8459  oe0m1  8533  sucdom2OLD  9096  sdomdif  9139  sucdom2  9217  php3  9223  php3OLD  9233  isinf  9268  isinfOLD  9269  unxpwdom2  9602  frind  9764  fin23lem26  10339  fin23lem21  10353  fin1a2lem13  10426  zornn0g  10519  fpwwe2lem12  10656  fpwwe2  10657  isumltss  15864  rpnnen2lem12  16243  symgsssg  19448  symgfisg  19449  psgnunilem5  19475  lspsnat  21106  lsppratlem6  21113  lspprat  21114  lbsextlem4  21122  cnsubrg  21395  opsrtoslem2  22014  psdmullem  22103  0ntr  23009  cmpfi  23346  dfconn2  23357  filconn  23821  cfinfil  23831  ufileu  23857  alexsublem  23982  ptcmplem2  23991  ptcmplem3  23992  restmetu  24509  reconnlem1  24766  bcthlem5  25280  itg10  25641  limcnlp  25831  noextendseq  27631  sltlpss  27871  upgrex  29071  uvtx01vtx  29376  ex-dif  30404  strlem1  32231  difininv  32498  eqdif  32500  difioo  32759  pmtrcnelor  33102  baselcarsg  34338  difelcarsg  34342  sibfof  34372  sitg0  34378  chtvalz  34661  onsucconni  36455  topdifinfeq  37368  nlpineqsn  37426  fdc  37769  setindtr  43048  oe0rif  43309  cantnfresb  43348  relnonrel  43611  inaex  44321  caragenunidm  46537