Theorem ssdif0 4366

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 3961	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3968	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4350	. 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 3948   ⊆ wss 3951  ∅c0 4333

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 2708

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 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968  df-nul 4334

This theorem is referenced by:  difn0  4367  pssdifn0  4368  difidALT  4377  vdif0  4469  difrab0eq  4470  difin0  4474  symdifv  5086  frpoind  6363  wfiOLD  6372  ordintdif  6434  dffv2  7004  fndifnfp  7196  tfi  7874  peano5  7915  frrlem13  8323  frrlem14  8324  wfrlem8OLD  8356  wfrlem16OLD  8364  tz7.49  8485  oe0m1  8559  sucdom2OLD  9122  sdomdif  9165  sucdom2  9243  php3  9249  php3OLD  9261  isinf  9296  isinfOLD  9297  unxpwdom2  9628  frind  9790  fin23lem26  10365  fin23lem21  10379  fin1a2lem13  10452  zornn0g  10545  fpwwe2lem12  10682  fpwwe2  10683  isumltss  15884  rpnnen2lem12  16261  symgsssg  19485  symgfisg  19486  psgnunilem5  19512  lspsnat  21147  lsppratlem6  21154  lspprat  21155  lbsextlem4  21163  cnsubrg  21445  opsrtoslem2  22080  psdmullem  22169  0ntr  23079  cmpfi  23416  dfconn2  23427  filconn  23891  cfinfil  23901  ufileu  23927  alexsublem  24052  ptcmplem2  24061  ptcmplem3  24062  restmetu  24583  reconnlem1  24848  bcthlem5  25362  itg10  25723  limcnlp  25913  noextendseq  27712  sltlpss  27945  upgrex  29109  uvtx01vtx  29414  ex-dif  30442  strlem1  32269  difininv  32536  eqdif  32538  difioo  32784  pmtrcnelor  33111  baselcarsg  34308  difelcarsg  34312  sibfof  34342  sitg0  34348  chtvalz  34644  onsucconni  36438  topdifinfeq  37351  nlpineqsn  37409  fdc  37752  setindtr  43036  oe0rif  43298  cantnfresb  43337  relnonrel  43600  inaex  44316  caragenunidm  46523