Theorem sseq0 4426

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 4035	. . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅))
2		ss0 4425	. . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
3	1, 2	biimtrdi 253	. 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅))
4	3	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3976  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-ss 3993  df-nul 4353

This theorem is referenced by:  ssn0  4427  ssdifin0  4509  disjxiun  5163  f1un  6882  fsetexb  8922  undomOLD  9126  infn0  9368  fieq0  9490  infdifsn  9726  cantnff  9743  tc00  9817  hashun3  14433  strleun  17204  dmdprdsplit2lem  20089  2idlval  21284  ocvval  21708  pjfval  21749  opsrle  22088  pf1rcl  22374  en2top  23013  nrmsep  23386  isnrm3  23388  regsep2  23405  xkohaus  23682  kqdisj  23761  regr1lem  23768  alexsublem  24073  reconnlem1  24867  metdstri  24892  iundisj2  25603  left0s  27949  right0s  27950  0clwlk0  30164  disjxpin  32610  iundisj2f  32612  iundisj2fi  32802  1arithufdlem4  33540  cvmsss2  35242  cldbnd  36292  cntotbnd  37756  nna4b4nsq  42615  mapfzcons1  42673  onfrALTlem2  44517  onfrALTlem2VD  44860  nnuzdisj  45270  ssdisjd  48539  ssdisjdr  48540  sepnsepolem2  48602  sepnsepo  48603