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

Theorem rexv 3124
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 2813 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 3112 . . . 4  |-  x  e. 
_V
32biantrur 506 . . 3  |-  ( ph  <->  ( x  e.  _V  /\  ph ) )
43exbii 1668 . 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 1613    e. wcel 1819   E.wrex 2808   _Vcvv 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-12 1855  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-rex 2813  df-v 3111
This theorem is referenced by:  rexcom4  3129  spesbc  3416  exopxfr  5156  dfco2  5512  dfco2a  5513  dffv2  5946  finacn  8448  ac6s2  8883  ptcmplem3  20679  ustn0  20848  hlimeui  26284  rexcom4f  27502  isrnsigaOLD  28273  isrnsiga  28274  prdstotbnd  30452  ac6s3f  30741  moxfr  30786  eldioph2b  30858  kelac1  31171  cbvexsv  33420
  Copyright terms: Public domain W3C validator