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  19381  symgfisg  19382  psgnunilem5  19408  lspsnat  21087  lsppratlem6  21094  lspprat  21095  lbsextlem4  21103  cnsubrg  21369  opsrtoslem2  21996  psdmullem  22085  0ntr  22991  cmpfi  23328  dfconn2  23339  filconn  23803  cfinfil  23813  ufileu  23839  alexsublem  23964  ptcmplem2  23973  ptcmplem3  23974  restmetu  24491  reconnlem1  24748  bcthlem5  25261  itg10  25622  limcnlp  25812  noextendseq  27612  sltlpss  27857  upgrex  29072  uvtx01vtx  29377  ex-dif  30402  strlem1  32229  difininv  32496  eqdif  32498  difioo  32755  pmtrcnelor  33063  baselcarsg  34290  difelcarsg  34294  sibfof  34324  sitg0  34330  chtvalz  34613  onvf1odlem2  35084  onsucconni  36418  topdifinfeq  37331  nlpineqsn  37389  fdc  37732  setindtr  43006  oe0rif  43267  cantnfresb  43306  relnonrel  43569  inaex  44279  caragenunidm  46499