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

Theorem rexv 2985
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 2719 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 2973 . . . 4  |-  x  e. 
_V
32biantrur 503 . . 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 1761   E.wrex 2714   _Vcvv 2970
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 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-rex 2719  df-v 2972
This theorem is referenced by:  rexcom4  2990  spesbc  3276  exopxfr  4979  dfco2  5334  dfco2a  5335  dffv2  5761  finacn  8216  ac6s2  8651  ptcmplem3  19585  ustn0  19754  hlimeui  24578  rexcom4f  25796  isrnsigaOLD  26491  isrnsiga  26492  prdstotbnd  28618  ac6s3f  28908  moxfr  28953  eldioph2b  29026  kelac1  29341  cbvexsv  31088
  Copyright terms: Public domain W3C validator