Theorem ssdif0 4277

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 405	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3891	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 338	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4258	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  difn0  4278  pssdifn0  4279  difid  4284  vdif0  4376  difrab0eq  4377  difin0  4380  symdifv  4971  wfi  6149  ordintdif  6208  dffv2  6733  fndifnfp  6915  tfi  7548  peano5  7585  wfrlem8  7945  wfrlem16  7953  tz7.49  8064  oe0m1  8129  sucdom2  8610  sdomdif  8649  php3  8687  isinf  8715  unxpwdom2  9036  fin23lem26  9736  fin23lem21  9750  fin1a2lem13  9823  zornn0g  9916  fpwwe2lem13  10053  fpwwe2  10054  isumltss  15195  rpnnen2lem12  15570  symgsssg  18587  symgfisg  18588  psgnunilem5  18614  lspsnat  19910  lsppratlem6  19917  lspprat  19918  lbsextlem4  19926  cnsubrg  20151  opsrtoslem2  20724  0ntr  21676  cmpfi  22013  dfconn2  22024  filconn  22488  cfinfil  22498  ufileu  22524  alexsublem  22649  ptcmplem2  22658  ptcmplem3  22659  restmetu  23177  reconnlem1  23431  bcthlem5  23932  itg10  24292  limcnlp  24481  upgrex  26885  uvtx01vtx  27187  ex-dif  28208  strlem1  30033  difininv  30288  eqdif  30290  difioo  30531  pmtrcnelor  30785  baselcarsg  31674  difelcarsg  31678  sibfof  31708  sitg0  31714  chtvalz  32010  frpoind  33193  frind  33198  frrlem13  33248  frrlem14  33249  noextendseq  33287  onsucconni  33898  topdifinfeq  34767  nlpineqsn  34825  fdc  35183  setindtr  39965  relnonrel  40287  inaex  41005  caragenunidm  43147