Theorem ssdif0 4325

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 3921	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3928	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4309	. 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 3908   ⊆ wss 3911  ∅c0 4292

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 3446  df-dif 3914  df-ss 3928  df-nul 4293

This theorem is referenced by:  difn0  4326  pssdifn0  4327  difidALT  4336  vdif0  4428  difrab0eq  4429  difin0  4433  symdifv  5045  frpoind  6303  ordintdif  6371  dffv2  6938  fndifnfp  7132  tfi  7809  peano5  7849  frrlem13  8254  frrlem14  8255  tz7.49  8390  oe0m1  8462  sdomdif  9066  sucdom2  9144  php3  9150  isinf  9183  isinfOLD  9184  unxpwdom2  9517  frind  9679  fin23lem26  10254  fin23lem21  10268  fin1a2lem13  10341  zornn0g  10434  fpwwe2lem12  10571  fpwwe2  10572  isumltss  15790  rpnnen2lem12  16169  symgsssg  19373  symgfisg  19374  psgnunilem5  19400  lspsnat  21031  lsppratlem6  21038  lspprat  21039  lbsextlem4  21047  cnsubrg  21320  opsrtoslem2  21939  psdmullem  22028  0ntr  22934  cmpfi  23271  dfconn2  23282  filconn  23746  cfinfil  23756  ufileu  23782  alexsublem  23907  ptcmplem2  23916  ptcmplem3  23917  restmetu  24434  reconnlem1  24691  bcthlem5  25204  itg10  25565  limcnlp  25755  noextendseq  27555  sltlpss  27795  upgrex  28995  uvtx01vtx  29300  ex-dif  30325  strlem1  32152  difininv  32419  eqdif  32421  difioo  32678  pmtrcnelor  33021  baselcarsg  34270  difelcarsg  34274  sibfof  34304  sitg0  34310  chtvalz  34593  onvf1odlem2  35064  onsucconni  36398  topdifinfeq  37311  nlpineqsn  37369  fdc  37712  setindtr  42986  oe0rif  43247  cantnfresb  43286  relnonrel  43549  inaex  44259  caragenunidm  46479