Theorem sseq0 4351

Description: A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
sseq0	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Proof of Theorem sseq0

Step	Hyp	Ref	Expression
1		sseq2 3959	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4350	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	biimtrdi 253	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3900  ∅c0 4281

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-dif 3903  df-ss 3917  df-nul 4282

This theorem is referenced by:  ssn0  4352  ssdifin0  4434  disjxiun  5086  f1un  6779  fsetexb  8783  infn0  9181  fieq0  9300  infdifsn  9542  cantnff  9559  tc00  9633  hashun3  14283  strleun  17060  dmdprdsplit2lem  19952  2idlval  21181  ocvval  21597  pjfval  21636  opsrle  21975  pf1rcl  22257  en2top  22893  nrmsep  23265  isnrm3  23267  regsep2  23284  xkohaus  23561  kqdisj  23640  regr1lem  23647  alexsublem  23952  reconnlem1  24735  metdstri  24760  iundisj2  25470  left0s  27831  right0s  27832  0clwlk0  30102  disjxpin  32558  iundisj2f  32560  iundisj2fi  32769  1arithufdlem4  33502  cvmsss2  35286  cldbnd  36339  cntotbnd  37815  nna4b4nsq  42672  mapfzcons1  42729  onfrALTlem2  44558  onfrALTlem2VD  44900  nnuzdisj  45373  ssdisjd  48818  ssdisjdr  48819  sepnsepolem2  48933  sepnsepo  48934  resccat  49085