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

Theorem eq0rdv 4124
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 119 . . 3 (𝜑 → (𝑥𝐴𝑥 ∈ ∅))
32ssrdv 3759 . 2 (𝜑𝐴 ⊆ ∅)
4 ss0 4119 . 2 (𝐴 ⊆ ∅ → 𝐴 = ∅)
53, 4syl 17 1 (𝜑𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1631  wcel 2145  wss 3724  c0 4064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3727  df-in 3731  df-ss 3738  df-nul 4065
This theorem is referenced by:  map0b  8050  disjen  8274  mapdom1  8282  pwxpndom2  9690  fzdisj  12576  smu01lem  15416  prmreclem5  15832  vdwap0  15888  natfval  16814  fucbas  16828  fuchom  16829  coafval  16922  efgval  18338  lsppratlem6  19368  lbsextlem4  19377  psrvscafval  19606  cfinufil  21953  ufinffr  21954  fin1aufil  21957  bldisj  22424  reconnlem1  22850  pcofval  23030  bcthlem5  23345  volfiniun  23536  fta1g  24148  fta1  24284  rpvmasum  25437  bj-projval  33316  finxpnom  33576  ipo0  39179  ifr0  39180  limclner  40402
  Copyright terms: Public domain W3C validator