Theorem ssdif0 3942

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 440	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3584	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 325	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1747	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3591	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 3929	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 292	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481   = wceq 1483   ∈ wcel 1990   ∖ cdif 3571   ⊆ wss 3574  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  difn0  3943  pssdifn0  3944  difid  3948  vdif0  4037  difrab0eq  4038  difin0  4041  symdifv  4598  wfi  5713  ordintdif  5774  dffv2  6271  fndifnfp  6442  tfi  7053  peano5  7089  wfrlem8  7422  wfrlem16  7430  tz7.49  7540  oe0m1  7601  sdomdif  8108  php3  8146  sucdom2  8156  isinf  8173  unxpwdom2  8493  fin23lem26  9147  fin23lem21  9161  fin1a2lem13  9234  zornn0g  9327  fpwwe2lem13  9464  fpwwe2  9465  isumltss  14580  rpnnen2lem12  14954  symgsssg  17887  symgfisg  17888  psgnunilem5  17914  lspsnat  19145  lsppratlem6  19152  lspprat  19153  lbsextlem4  19161  opsrtoslem2  19485  cnsubrg  19806  0ntr  20875  cmpfi  21211  dfconn2  21222  filconn  21687  cfinfil  21697  ufileu  21723  alexsublem  21848  ptcmplem2  21857  ptcmplem3  21858  restmetu  22375  reconnlem1  22629  bcthlem5  23125  itg10  23455  limcnlp  23642  upgrex  25987  uvtxa01vtx0  26297  ex-dif  27280  strlem1  29109  difininv  29354  difioo  29544  baselcarsg  30368  difelcarsg  30372  sibfof  30402  sitg0  30408  chtvalz  30707  frind  31740  noextendseq  31820  onsucconni  32436  topdifinfeq  33198  fdc  33541  setindtr  37591  relnonrel  37893  caragenunidm  40722