Theorem ssdif0 4321

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570   ∈ wcel 2143   ∖ cdif 3902   ⊆ wss 3905  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-ss 3922  df-nul 4287

This theorem is referenced by:  difn0  4322  pssdifn0  4323  inssdif0  4329  difidALT  4333  vdif0  4429  difrab0eq  4430  difin0  4435  symdifv  5052  frpoind  6343  ordintdif  6412  dffv2  6976  fndifnfp  7174  tfi  7845  peano5  7886  frrlem13  8291  frrlem14  8292  tz7.49  8428  oe0m1  8502  sdomdif  9109  sucdom2  9183  php3  9189  isinf  9221  unxpwdom2  9546  frind  9718  fin23lem26  10304  fin23lem21  10318  fin1a2lem13  10391  zornn0g  10484  fpwwe2lem12  10622  fpwwe2  10623  isumltss  15898  rpnnen2lem12  16276  chnccat  18677  symgsssg  19532  symgfisg  19533  psgnunilem5  19559  lspsnat  21269  lsppratlem6  21276  lspprat  21277  lbsextlem4  21285  cnsubrg  21577  opsrtoslem2  22207  psdmullem  22328  0ntr  23228  cmpfi  23565  dfconn2  23576  filconn  24040  cfinfil  24050  ufileu  24076  alexsublem  24201  ptcmplem2  24210  ptcmplem3  24211  restmetu  24727  reconnlem1  24984  bcthlem5  25487  itg10  25847  limcnlp  26037  noextendseq  27831  ltslpss  28101  upgrex  29442  uvtx01vtx  29747  ex-dif  30774  strlem1  32602  difininv  32863  eqdif  32865  difioo  33127  pmtrcnelor  33411  dflringlem3  33786  dflring4  33788  baselcarsg  34696  difelcarsg  34700  sibfof  34730  sitg0  34736  chtvalz  35016  onvf1odlem2  35588  onsucconni  36948  ttcwf2  37036  topdifinfeq  37996  nlpineqsn  38054  fdc  38396  setindtr  43751  oe0rif  44012  cantnfresb  44051  relnonrel  44313  inaex  45007  caragenunidm  47222