Theorem ssdif0 4307

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 3900	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3907	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4291	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ∖ cdif 3887   ⊆ wss 3890  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907  df-nul 4275

This theorem is referenced by:  difn0  4308  pssdifn0  4309  difidALT  4318  vdif0  4410  difrab0eq  4411  difin0  4415  symdifv  5029  frpoind  6301  ordintdif  6369  dffv2  6930  fndifnfp  7125  tfi  7798  peano5  7838  frrlem13  8242  frrlem14  8243  tz7.49  8378  oe0m1  8450  sdomdif  9057  sucdom2  9131  php3  9137  isinf  9169  unxpwdom2  9497  frind  9668  fin23lem26  10241  fin23lem21  10255  fin1a2lem13  10328  zornn0g  10421  fpwwe2lem12  10559  fpwwe2  10560  isumltss  15807  rpnnen2lem12  16186  chnccat  18586  symgsssg  19436  symgfisg  19437  psgnunilem5  19463  lspsnat  21138  lsppratlem6  21145  lspprat  21146  lbsextlem4  21154  cnsubrg  21420  opsrtoslem2  22047  psdmullem  22144  0ntr  23049  cmpfi  23386  dfconn2  23397  filconn  23861  cfinfil  23871  ufileu  23897  alexsublem  24022  ptcmplem2  24031  ptcmplem3  24032  restmetu  24548  reconnlem1  24805  bcthlem5  25308  itg10  25668  limcnlp  25858  noextendseq  27648  ltslpss  27917  upgrex  29178  uvtx01vtx  29483  ex-dif  30511  strlem1  32339  difininv  32605  eqdif  32607  difioo  32873  pmtrcnelor  33170  baselcarsg  34469  difelcarsg  34473  sibfof  34503  sitg0  34509  chtvalz  34792  onvf1odlem2  35305  onsucconni  36638  ttcwf2  36726  topdifinfeq  37683  nlpineqsn  37741  fdc  38083  setindtr  43473  oe0rif  43734  cantnfresb  43773  relnonrel  44035  inaex  44745  caragenunidm  46957