Theorem ssdif0 4306

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 3899	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3906	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4290	. 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 3886   ⊆ wss 3889  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906  df-nul 4274

This theorem is referenced by:  difn0  4307  pssdifn0  4308  difidALT  4317  vdif0  4409  difrab0eq  4410  difin0  4414  symdifv  5028  frpoind  6306  ordintdif  6374  dffv2  6935  fndifnfp  7131  tfi  7804  peano5  7844  frrlem13  8248  frrlem14  8249  tz7.49  8384  oe0m1  8456  sdomdif  9063  sucdom2  9137  php3  9143  isinf  9175  unxpwdom2  9503  frind  9674  fin23lem26  10247  fin23lem21  10261  fin1a2lem13  10334  zornn0g  10427  fpwwe2lem12  10565  fpwwe2  10566  isumltss  15813  rpnnen2lem12  16192  chnccat  18592  symgsssg  19442  symgfisg  19443  psgnunilem5  19469  lspsnat  21143  lsppratlem6  21150  lspprat  21151  lbsextlem4  21159  cnsubrg  21407  opsrtoslem2  22034  psdmullem  22131  0ntr  23036  cmpfi  23373  dfconn2  23384  filconn  23848  cfinfil  23858  ufileu  23884  alexsublem  24009  ptcmplem2  24018  ptcmplem3  24019  restmetu  24535  reconnlem1  24792  bcthlem5  25295  itg10  25655  limcnlp  25845  noextendseq  27631  ltslpss  27900  upgrex  29161  uvtx01vtx  29466  ex-dif  30493  strlem1  32321  difininv  32587  eqdif  32589  difioo  32855  pmtrcnelor  33152  baselcarsg  34450  difelcarsg  34454  sibfof  34484  sitg0  34490  chtvalz  34773  onvf1odlem2  35286  onsucconni  36619  ttcwf2  36707  topdifinfeq  37666  nlpineqsn  37724  fdc  38066  setindtr  43452  oe0rif  43713  cantnfresb  43752  relnonrel  44014  inaex  44724  caragenunidm  46936