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

Theorem rexv 3123
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 2815 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 3111 . . . 4  |-  x  e. 
_V
32biantrur 506 . . 3  |-  ( ph  <->  ( x  e.  _V  /\  ph ) )
43exbii 1639 . 2  |-  ( E. x ph  <->  E. x
( x  e.  _V  /\ 
ph ) )
51, 4bitr4i 252 1  |-  ( E. x  e.  _V  ph  <->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1591    e. wcel 1762   E.wrex 2810   _Vcvv 3108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-rex 2815  df-v 3110
This theorem is referenced by:  rexcom4  3128  spesbc  3419  exopxfr  5139  dfco2  5499  dfco2a  5500  dffv2  5933  finacn  8422  ac6s2  8857  ptcmplem3  20284  ustn0  20453  hlimeui  25822  rexcom4f  27040  isrnsigaOLD  27740  isrnsiga  27741  prdstotbnd  29882  ac6s3f  30172  moxfr  30217  eldioph2b  30289  kelac1  30604  cbvexsv  32276
  Copyright terms: Public domain W3C validator