Theorem ssdif0 4329

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ∖ cdif 3911   ⊆ wss 3914  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931  df-nul 4297

This theorem is referenced by:  difn0  4330  pssdifn0  4331  difidALT  4340  vdif0  4432  difrab0eq  4433  difin0  4437  symdifv  5050  frpoind  6315  ordintdif  6383  dffv2  6956  fndifnfp  7150  tfi  7829  peano5  7869  frrlem13  8277  frrlem14  8278  tz7.49  8413  oe0m1  8485  sdomdif  9089  sucdom2  9167  php3  9173  isinf  9207  isinfOLD  9208  unxpwdom2  9541  frind  9703  fin23lem26  10278  fin23lem21  10292  fin1a2lem13  10365  zornn0g  10458  fpwwe2lem12  10595  fpwwe2  10596  isumltss  15814  rpnnen2lem12  16193  symgsssg  19397  symgfisg  19398  psgnunilem5  19424  lspsnat  21055  lsppratlem6  21062  lspprat  21063  lbsextlem4  21071  cnsubrg  21344  opsrtoslem2  21963  psdmullem  22052  0ntr  22958  cmpfi  23295  dfconn2  23306  filconn  23770  cfinfil  23780  ufileu  23806  alexsublem  23931  ptcmplem2  23940  ptcmplem3  23941  restmetu  24458  reconnlem1  24715  bcthlem5  25228  itg10  25589  limcnlp  25779  noextendseq  27579  sltlpss  27819  upgrex  29019  uvtx01vtx  29324  ex-dif  30352  strlem1  32179  difininv  32446  eqdif  32448  difioo  32705  pmtrcnelor  33048  baselcarsg  34297  difelcarsg  34301  sibfof  34331  sitg0  34337  chtvalz  34620  onvf1odlem2  35091  onsucconni  36425  topdifinfeq  37338  nlpineqsn  37396  fdc  37739  setindtr  43013  oe0rif  43274  cantnfresb  43313  relnonrel  43576  inaex  44286  caragenunidm  46506