Theorem ssdif0 4317

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 407	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 4052	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 338	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4300	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900   ∖ cdif 4048  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050  df-nul 4282

This theorem is used by:  difn0  4318  pssdifn0  4319  inssdif0  4325  difidALT  4329  vdif0  4425  difrab0eq  4426  difin0  4431  symdifv  5051  frpoind  6371  ordintdif  6440  dffv2  7011  fndifnfp  7212  tfi  7898  peano5  7939  frrlem13  8354  frrlem14  8355  tz7.49  8493  oe0m1  8567  sdomdif  9182  sucdom2  9256  php3  9262  isinf  9294  unxpwdom2  9619  frind  9791  fin23lem26  10442  fin23lem21  10456  fin1a2lem13  10529  zornn0g  10622  fpwwe2lem12  10766  fpwwe2  10767  isumltss  16061  rpnnen2lem12  16437  chnccat  18850  symgsssg  19732  symgfisg  19733  psgnunilem5  19759  lspsnat  21474  lsppratlem6  21481  lspprat  21482  lbsextlem4  21490  cnsubrg  21787  opsrtoslem2  22420  psdmullem  22541  0ntr  23444  cmpfi  23781  dfconn2  23792  filconn  24257  cfinfil  24267  ufileu  24293  alexsublem  24418  ptcmplem2  24427  ptcmplem3  24428  restmetu  24944  reconnlem1  25201  bcthlem5  25704  itg10  26064  limcnlp  26253  noextendseq  28081  ltslpss  28351  upgrex  29727  uvtx01vtx  30035  ex-dif  31081  strlem1  32909  difininv  33212  eqdif  33214  difioo  33470  pmtrcnelor  33751  dflringlem3  34132  dflring4  34134  baselcarsg  35049  difelcarsg  35053  sibfof  35083  sitg0  35089  chtvalz  35369  onvf1odlem2  36073  onsucconni  37440  ttcwf2  37528  topdifinfeq  38541  nlpineqsn  38599  fdc  38945  setindtr  44297  oe0rif  44548  cantnfresb  44587  relnonrel  44848  inaex  45542  caragenunidm  47791