Theorem ssdif0 4360

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 3955	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 335	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1814	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3965	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4340	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1532   = wceq 1534   ∈ wcel 2099   ∖ cdif 3942   ⊆ wss 3945  ∅c0 4319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-dif 3948  df-in 3952  df-ss 3962  df-nul 4320

This theorem is referenced by:  difn0  4361  pssdifn0  4362  difidALT  4368  vdif0  4465  difrab0eq  4466  difin0  4470  symdifv  5084  frpoind  6343  wfiOLD  6352  ordintdif  6414  dffv2  6988  fndifnfp  7180  tfi  7852  peano5  7894  peano5OLD  7895  frrlem13  8298  frrlem14  8299  wfrlem8OLD  8331  wfrlem16OLD  8339  tz7.49  8460  oe0m1  8536  sucdom2OLD  9101  sdomdif  9144  sucdom2  9225  php3  9231  php3OLD  9243  isinf  9279  isinfOLD  9280  unxpwdom2  9606  frind  9768  fin23lem26  10343  fin23lem21  10357  fin1a2lem13  10430  zornn0g  10523  fpwwe2lem12  10660  fpwwe2  10661  isumltss  15821  rpnnen2lem12  16196  symgsssg  19416  symgfisg  19417  psgnunilem5  19443  lspsnat  21027  lsppratlem6  21034  lspprat  21035  lbsextlem4  21043  cnsubrg  21354  opsrtoslem2  21994  psdmullem  22083  0ntr  22969  cmpfi  23306  dfconn2  23317  filconn  23781  cfinfil  23791  ufileu  23817  alexsublem  23942  ptcmplem2  23951  ptcmplem3  23952  restmetu  24473  reconnlem1  24736  bcthlem5  25250  itg10  25611  limcnlp  25801  noextendseq  27594  sltlpss  27827  upgrex  28899  uvtx01vtx  29204  ex-dif  30227  strlem1  32054  difininv  32307  eqdif  32310  difioo  32545  pmtrcnelor  32809  baselcarsg  33921  difelcarsg  33925  sibfof  33955  sitg0  33961  chtvalz  34256  onsucconni  35916  topdifinfeq  36824  nlpineqsn  36882  fdc  37213  setindtr  42436  oe0rif  42705  cantnfresb  42744  relnonrel  43008  inaex  43725  caragenunidm  45887

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »