MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eq0rdv Structured version   Visualization version   GIF version

Theorem eq0rdv 3951
Description: Deduction rule for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
Hypothesis
Ref Expression
eq0rdv.1 (𝜑 → ¬ 𝑥𝐴)
Assertion
Ref Expression
eq0rdv (𝜑𝐴 = ∅)
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Proof of Theorem eq0rdv
StepHypRef Expression
1 eq0rdv.1 . . . 4 (𝜑 → ¬ 𝑥𝐴)
21pm2.21d 118 . . 3 (𝜑 → (𝑥𝐴𝑥 ∈ ∅))
32ssrdv 3589 . 2 (𝜑𝐴 ⊆ ∅)
4 ss0 3946 . 2 (𝐴 ⊆ ∅ → 𝐴 = ∅)
53, 4syl 17 1 (𝜑𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wcel 1987  wss 3555  c0 3891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3558  df-in 3562  df-ss 3569  df-nul 3892
This theorem is referenced by:  map0b  7840  disjen  8061  mapdom1  8069  pwxpndom2  9431  fzdisj  12310  smu01lem  15131  prmreclem5  15548  vdwap0  15604  natfval  16527  fucbas  16541  fuchom  16542  coafval  16635  efgval  18051  lsppratlem6  19071  lbsextlem4  19080  psrvscafval  19309  cfinufil  21642  ufinffr  21643  fin1aufil  21646  bldisj  22113  reconnlem1  22537  pcofval  22718  bcthlem5  23033  volfiniun  23222  fta1g  23831  fta1  23967  rpvmasum  25115  bj-projval  32631  finxpnom  32870  ipo0  38135  ifr0  38136  limclner  39287
  Copyright terms: Public domain W3C validator