Theorem ssdif0 4294

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 3893	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 334	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1823	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3903	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4274	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539   ∈ wcel 2108   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  difn0  4295  pssdifn0  4296  difidALT  4302  vdif0  4399  difrab0eq  4400  difin0  4404  symdifv  5011  frpoind  6230  wfiOLD  6239  ordintdif  6300  dffv2  6845  fndifnfp  7030  tfi  7675  peano5  7714  peano5OLD  7715  frrlem13  8085  frrlem14  8086  wfrlem8OLD  8118  wfrlem16OLD  8126  tz7.49  8246  oe0m1  8313  sucdom2  8822  sdomdif  8861  php3  8899  isinf  8965  unxpwdom2  9277  frind  9439  fin23lem26  10012  fin23lem21  10026  fin1a2lem13  10099  zornn0g  10192  fpwwe2lem12  10329  fpwwe2  10330  isumltss  15488  rpnnen2lem12  15862  symgsssg  18990  symgfisg  18991  psgnunilem5  19017  lspsnat  20322  lsppratlem6  20329  lspprat  20330  lbsextlem4  20338  cnsubrg  20570  opsrtoslem2  21173  0ntr  22130  cmpfi  22467  dfconn2  22478  filconn  22942  cfinfil  22952  ufileu  22978  alexsublem  23103  ptcmplem2  23112  ptcmplem3  23113  restmetu  23632  reconnlem1  23895  bcthlem5  24397  itg10  24757  limcnlp  24947  upgrex  27365  uvtx01vtx  27667  ex-dif  28688  strlem1  30513  difininv  30765  eqdif  30767  difioo  31005  pmtrcnelor  31262  baselcarsg  32173  difelcarsg  32177  sibfof  32207  sitg0  32213  chtvalz  32509  noextendseq  33797  sltlpss  34014  onsucconni  34553  topdifinfeq  35448  nlpineqsn  35506  fdc  35830  setindtr  40762  relnonrel  41084  inaex  41804  caragenunidm  43936