Theorem ssdif0 4172

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 392	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3802	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 327	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1863	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3809	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4157	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 295	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1599   = wceq 1601   ∈ wcel 2107   ∖ cdif 3789   ⊆ wss 3792  ∅c0 4141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-dif 3795  df-in 3799  df-ss 3806  df-nul 4142

This theorem is referenced by:  difn0  4173  pssdifn0  4174  difid  4179  vdif0  4261  difrab0eq  4262  difin0  4265  symdifv  4833  wfi  5968  ordintdif  6027  dffv2  6533  fndifnfp  6711  tfi  7333  peano5  7369  wfrlem8  7707  wfrlem16  7715  tz7.49  7825  oe0m1  7887  sdomdif  8398  php3  8436  sucdom2  8446  isinf  8463  unxpwdom2  8784  fin23lem26  9484  fin23lem21  9498  fin1a2lem13  9571  zornn0g  9664  fpwwe2lem13  9801  fpwwe2  9802  isumltss  14988  rpnnen2lem12  15362  symgsssg  18274  symgfisg  18275  psgnunilem5  18301  psgnunilem5OLD  18302  lspsnat  19545  lsppratlem6  19553  lspprat  19554  lbsextlem4  19562  opsrtoslem2  19885  cnsubrg  20206  0ntr  21287  cmpfi  21624  dfconn2  21635  filconn  22099  cfinfil  22109  ufileu  22135  alexsublem  22260  ptcmplem2  22269  ptcmplem3  22270  restmetu  22787  reconnlem1  23041  bcthlem5  23538  itg10  23896  limcnlp  24083  upgrex  26444  uvtx01vtx  26749  ex-dif  27859  strlem1  29685  difininv  29920  difioo  30112  baselcarsg  30970  difelcarsg  30974  sibfof  31004  sitg0  31010  chtvalz  31313  frpoind  32333  frind  32336  noextendseq  32413  onsucconni  33023  topdifinfeq  33796  fdc  34170  setindtr  38560  relnonrel  38860  caragenunidm  41659