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

Theorem eq0rdv 4354
Description: Deduction 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 121 . . 3 (𝜑 → (𝑥𝐴𝑥 ∈ ∅))
32ssrdv 3970 . 2 (𝜑𝐴 ⊆ ∅)
4 ss0 4349 . 2 (𝐴 ⊆ ∅ → 𝐴 = ∅)
53, 4syl 17 1 (𝜑𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wcel 2105  wss 3933  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-dif 3936  df-in 3940  df-ss 3949  df-nul 4289
This theorem is referenced by:  map0b  8436  disjen  8662  mapdom1  8670  pwxpndom2  10075  fzdisj  12922  smu01lem  15822  prmreclem5  16244  vdwap0  16300  natfval  17204  fucbas  17218  fuchom  17219  coafval  17312  efgval  18772  lsppratlem6  19853  lbsextlem4  19862  psrvscafval  20098  cfinufil  22464  ufinffr  22465  fin1aufil  22468  bldisj  22935  reconnlem1  23361  pcofval  23541  bcthlem5  23858  volfiniun  24075  fta1g  24688  fta1  24824  rpvmasum  26029  unblimceq0  33743  bj-projval  34205  finxpnom  34564  ipo0  40658  ifr0  40659  limclner  41808
  Copyright terms: Public domain W3C validator