Theorem ssdif0 4322

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 404	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3945	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 337	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1816	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3954	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4307	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 305	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1531   = wceq 1533   ∈ wcel 2110   ∖ cdif 3932   ⊆ wss 3935  ∅c0 4290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938  df-in 3942  df-ss 3951  df-nul 4291

This theorem is referenced by:  difn0  4323  pssdifn0  4324  difid  4329  vdif0  4417  difrab0eq  4418  difin0  4421  symdifv  5000  wfi  6175  ordintdif  6234  dffv2  6750  fndifnfp  6932  tfi  7562  peano5  7599  wfrlem8  7956  wfrlem16  7964  tz7.49  8075  oe0m1  8140  sdomdif  8659  php3  8697  sucdom2  8708  isinf  8725  unxpwdom2  9046  fin23lem26  9741  fin23lem21  9755  fin1a2lem13  9828  zornn0g  9921  fpwwe2lem13  10058  fpwwe2  10059  isumltss  15197  rpnnen2lem12  15572  symgsssg  18589  symgfisg  18590  psgnunilem5  18616  lspsnat  19911  lsppratlem6  19918  lspprat  19919  lbsextlem4  19927  opsrtoslem2  20259  cnsubrg  20599  0ntr  21673  cmpfi  22010  dfconn2  22021  filconn  22485  cfinfil  22495  ufileu  22521  alexsublem  22646  ptcmplem2  22655  ptcmplem3  22656  restmetu  23174  reconnlem1  23428  bcthlem5  23925  itg10  24283  limcnlp  24470  upgrex  26871  uvtx01vtx  27173  ex-dif  28196  strlem1  30021  difininv  30273  eqdif  30275  difioo  30499  pmtrcnelor  30730  baselcarsg  31559  difelcarsg  31563  sibfof  31593  sitg0  31599  chtvalz  31895  frpoind  33075  frind  33080  frrlem13  33130  frrlem14  33131  noextendseq  33169  onsucconni  33780  topdifinfeq  34625  nlpineqsn  34683  fdc  35014  setindtr  39614  relnonrel  39940  inaex  40626  caragenunidm  42784