MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexv Unicode version

Theorem rexv 2938
Description: An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
Assertion
Ref Expression
rexv  |-  ( E. x  e.  _V  ph  <->  E. x ph )

Proof of Theorem rexv
StepHypRef Expression
1 df-rex 2680 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 2927 . . . 4  |-  x  e. 
_V
32biantrur 493 . . 3  |-  ( ph  <->  ( x  e.  _V  /\  ph ) )
43exbii 1589 . 2  |-  ( E. x ph  <->  E. x
( x  e.  _V  /\ 
ph ) )
51, 4bitr4i 244 1  |-  ( E. x  e.  _V  ph  <->  E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    e. wcel 1721   E.wrex 2675   _Vcvv 2924
This theorem is referenced by:  rexcom4  2943  spesbc  3210  dfco2  5336  dfco2a  5337  dffv2  5763  exopxfr  6377  finacn  7895  ac6s2  8330  ptcmplem3  18046  ustn0  18211  hlimeui  22704  rexcom4f  23927  isrnsigaOLD  24456  isrnsiga  24457  prdstotbnd  26401  moxfr  26631  eldioph2b  26719  kelac1  27037  cbvexsv  28352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-rex 2680  df-v 2926
  Copyright terms: Public domain W3C validator