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

Theorem rexv 3096
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 2781 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 3084 . . . 4  |-  x  e. 
_V
32biantrur 508 . . 3  |-  ( ph  <->  ( x  e.  _V  /\  ph ) )
43exbii 1712 . 2  |-  ( E. x ph  <->  E. x
( x  e.  _V  /\ 
ph ) )
51, 4bitr4i 255 1  |-  ( E. x  e.  _V  ph  <->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wex 1659    e. wcel 1868   E.wrex 2776   _Vcvv 3081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-12 1905  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-rex 2781  df-v 3083
This theorem is referenced by:  rexcom4  3101  spesbc  3381  exopxfr  4993  dfco2  5349  dfco2a  5350  dffv2  5950  finacn  8481  ac6s2  8916  ptcmplem3  21055  ustn0  21221  hlimeui  26878  rexcom4f  28096  isrnsigaOLD  28929  isrnsiga  28930  prdstotbnd  32039  ac6s3f  32327  moxfr  35452  eldioph2b  35523  kelac1  35840  cbvexsv  36770
  Copyright terms: Public domain W3C validator