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

Theorem rex0 4318
Description: Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.)
Assertion
Ref Expression
rex0 ¬ ∃𝑥 ∈ ∅ 𝜑

Proof of Theorem rex0
StepHypRef Expression
1 noel 4291 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 119 . 2 (𝑥 ∈ ∅ → ¬ 𝜑)
32nrex 3074 1 ¬ ∃𝑥 ∈ ∅ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 2107  wrex 3070  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-dif 3914  df-nul 4284
This theorem is referenced by:  reu0  4319  rmo0  4320  0iun  5024  sup0riota  9406  cfeq0  10197  cfsuc  10198  hashge2el2difr  14386  cshws0  16979  addsrid  27298  muls01  27397  muls02  27398  mulsrid  27399  mulslid  27400  0ringirng  32420  dya2iocuni  32940  eulerpartlemgh  33035  0qs  36877  pmapglb2xN  38281  elpadd0  38318  sprsymrelfvlem  45768  ipolub00  47104
  Copyright terms: Public domain W3C validator