Theorem ssdif0 4323

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 404	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3946	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 337	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		dfss2 3955	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4308	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 305	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537   ∈ wcel 2114   ∖ cdif 3933   ⊆ wss 3936  ∅c0 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  difn0  4324  pssdifn0  4325  difid  4330  vdif0  4418  difrab0eq  4419  difin0  4422  symdifv  5008  wfi  6181  ordintdif  6240  dffv2  6756  fndifnfp  6938  tfi  7568  peano5  7605  wfrlem8  7962  wfrlem16  7970  tz7.49  8081  oe0m1  8146  sdomdif  8665  php3  8703  sucdom2  8714  isinf  8731  unxpwdom2  9052  fin23lem26  9747  fin23lem21  9761  fin1a2lem13  9834  zornn0g  9927  fpwwe2lem13  10064  fpwwe2  10065  isumltss  15203  rpnnen2lem12  15578  symgsssg  18595  symgfisg  18596  psgnunilem5  18622  lspsnat  19917  lsppratlem6  19924  lspprat  19925  lbsextlem4  19933  opsrtoslem2  20265  cnsubrg  20605  0ntr  21679  cmpfi  22016  dfconn2  22027  filconn  22491  cfinfil  22501  ufileu  22527  alexsublem  22652  ptcmplem2  22661  ptcmplem3  22662  restmetu  23180  reconnlem1  23434  bcthlem5  23931  itg10  24289  limcnlp  24476  upgrex  26877  uvtx01vtx  27179  ex-dif  28202  strlem1  30027  difininv  30279  eqdif  30281  difioo  30505  pmtrcnelor  30735  baselcarsg  31564  difelcarsg  31568  sibfof  31598  sitg0  31604  chtvalz  31900  frpoind  33080  frind  33085  frrlem13  33135  frrlem14  33136  noextendseq  33174  onsucconni  33785  topdifinfeq  34634  nlpineqsn  34692  fdc  35035  setindtr  39641  relnonrel  39967  inaex  40653  caragenunidm  42810