Theorem ssdif0 4314

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 407	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		eldif 3909	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	xchbinxr 338	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
4	3	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
5		df-ss 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
6		eq0 4297	. 2 ⊢ ((𝐴 ∖ 𝐵) = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ (𝐴 ∖ 𝐵))
7	4, 5, 6	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  difn0  4315  pssdifn0  4316  inssdif0  4322  difidALT  4326  vdif0  4422  difrab0eq  4423  difin0  4428  symdifv  5046  frpoind  6340  ordintdif  6409  dffv2  6973  fndifnfp  7174  tfi  7849  peano5  7890  frrlem13  8297  frrlem14  8298  tz7.49  8434  oe0m1  8508  sdomdif  9123  sucdom2  9197  php3  9203  isinf  9235  unxpwdom2  9560  frind  9732  fin23lem26  10327  fin23lem21  10341  fin1a2lem13  10414  zornn0g  10507  fpwwe2lem12  10651  fpwwe2  10652  isumltss  15937  rpnnen2lem12  16313  chnccat  18714  symgsssg  19594  symgfisg  19595  psgnunilem5  19621  lspsnat  21332  lsppratlem6  21339  lspprat  21340  lbsextlem4  21348  cnsubrg  21640  opsrtoslem2  22272  psdmullem  22393  0ntr  23296  cmpfi  23633  dfconn2  23644  filconn  24109  cfinfil  24119  ufileu  24145  alexsublem  24270  ptcmplem2  24279  ptcmplem3  24280  restmetu  24796  reconnlem1  25053  bcthlem5  25556  itg10  25916  limcnlp  26105  noextendseq  27903  ltslpss  28173  upgrex  29549  uvtx01vtx  29857  ex-dif  30903  strlem1  32731  difininv  32992  eqdif  32994  difioo  33253  pmtrcnelor  33531  dflringlem3  33906  dflring4  33908  baselcarsg  34817  difelcarsg  34821  sibfof  34851  sitg0  34857  chtvalz  35137  onvf1odlem2  35701  onsucconni  37056  ttcwf2  37144  topdifinfeq  38104  nlpineqsn  38162  fdc  38495  setindtr  43865  oe0rif  44126  cantnfresb  44165  relnonrel  44427  inaex  45121  caragenunidm  47336