Theorem ssdif0 4362

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 402	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3957	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 334	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3967	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4342	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541   ∈ wcel 2106   ∖ cdif 3944   ⊆ wss 3947  ∅c0 4321

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  difn0  4363  pssdifn0  4364  difidALT  4370  vdif0  4467  difrab0eq  4468  difin0  4472  symdifv  5088  frpoind  6340  wfiOLD  6349  ordintdif  6411  dffv2  6983  fndifnfp  7170  tfi  7838  peano5  7880  peano5OLD  7881  frrlem13  8279  frrlem14  8280  wfrlem8OLD  8312  wfrlem16OLD  8320  tz7.49  8441  oe0m1  8517  sucdom2OLD  9078  sdomdif  9121  sucdom2  9202  php3  9208  php3OLD  9220  isinf  9256  isinfOLD  9257  unxpwdom2  9579  frind  9741  fin23lem26  10316  fin23lem21  10330  fin1a2lem13  10403  zornn0g  10496  fpwwe2lem12  10633  fpwwe2  10634  isumltss  15790  rpnnen2lem12  16164  symgsssg  19329  symgfisg  19330  psgnunilem5  19356  lspsnat  20750  lsppratlem6  20757  lspprat  20758  lbsextlem4  20766  cnsubrg  20997  opsrtoslem2  21608  0ntr  22566  cmpfi  22903  dfconn2  22914  filconn  23378  cfinfil  23388  ufileu  23414  alexsublem  23539  ptcmplem2  23548  ptcmplem3  23549  restmetu  24070  reconnlem1  24333  bcthlem5  24836  itg10  25196  limcnlp  25386  noextendseq  27159  sltlpss  27390  upgrex  28341  uvtx01vtx  28643  ex-dif  29665  strlem1  31490  difininv  31742  eqdif  31744  difioo  31980  pmtrcnelor  32239  baselcarsg  33293  difelcarsg  33297  sibfof  33327  sitg0  33333  chtvalz  33629  onsucconni  35310  topdifinfeq  36219  nlpineqsn  36277  fdc  36601  setindtr  41748  oe0rif  42020  cantnfresb  42059  relnonrel  42323  inaex  43041  caragenunidm  45210