Theorem sseq0 4338

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 3948	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4337	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	biimtrdi 254	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ⊆ wss 3890  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-dif 3893  df-ss 3907  df-nul 4269

This theorem is referenced by:  ssn0  4339  ssdifin0  4420  disjxiun  5076  f1un  6794  fsetexb  8808  infn0  9209  fieq0  9331  infdifsn  9576  cantnff  9593  tc00  9665  hashun3  14344  strleun  17125  dmdprdsplit2lem  20020  2idlval  21251  ocvval  21649  pjfval  21688  opsrle  22030  pf1rcl  22342  en2top  22975  nrmsep  23347  isnrm3  23349  regsep2  23366  xkohaus  23643  kqdisj  23722  regr1lem  23729  alexsublem  24034  reconnlem1  24817  metdstri  24842  iundisj2  25541  left0s  27910  right0s  27911  0clwlk0  30227  disjxpin  32684  iundisj2f  32686  iundisj2fi  32896  1arithufdlem4  33637  cvmsss2  35503  cldbnd  36555  cntotbnd  38164  nna4b4nsq  43111  mapfzcons1  43167  onfrALTlem2  44991  onfrALTlem2VD  45333  nnuzdisj  45801  ssdisjd  49299  ssdisjdr  49300  sepnsepolem2  49414  sepnsepo  49415  resccat  49565