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

Theorem rexv 2930
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 2672 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 2919 . . . 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 2667   _Vcvv 2916
This theorem is referenced by:  rexcom4  2935  spesbc  3202  dfco2  5328  dfco2a  5329  dffv2  5755  exopxfr  6369  finacn  7887  ac6s2  8322  ptcmplem3  18038  ustn0  18203  hlimeui  22696  rexcom4f  23919  isrnsigaOLD  24448  isrnsiga  24449  prdstotbnd  26393  moxfr  26623  eldioph2b  26711  kelac1  27029  cbvexsv  28344
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 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-rex 2672  df-v 2918
  Copyright terms: Public domain W3C validator