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

Theorem eq0rdv 4361
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 3977 . 2 (𝜑𝐴 ⊆ ∅)
4 ss0 4356 . 2 (𝐴 ⊆ ∅ → 𝐴 = ∅)
53, 4syl 17 1 (𝜑𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wcel 2107  wss 3940  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-dif 3943  df-in 3947  df-ss 3956  df-nul 4296
This theorem is referenced by:  map0b  8437  disjen  8663  mapdom1  8671  pwxpndom2  10076  fzdisj  12924  smu01lem  15824  prmreclem5  16246  vdwap0  16302  natfval  17206  fucbas  17220  fuchom  17221  coafval  17314  efgval  18763  lsppratlem6  19844  lbsextlem4  19853  psrvscafval  20089  cfinufil  22452  ufinffr  22453  fin1aufil  22456  bldisj  22923  reconnlem1  23349  pcofval  23529  bcthlem5  23846  volfiniun  24063  fta1g  24676  fta1  24812  rpvmasum  26016  unblimceq0  33730  bj-projval  34192  finxpnom  34551  ipo0  40646  ifr0  40647  limclner  41797
  Copyright terms: Public domain W3C validator