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

Theorem rexv 3048
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 2762 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 3034 . . . 4  |-  x  e. 
_V
32biantrur 514 . . 3  |-  ( ph  <->  ( x  e.  _V  /\  ph ) )
43exbii 1726 . 2  |-  ( E. x ph  <->  E. x
( x  e.  _V  /\ 
ph ) )
51, 4bitr4i 260 1  |-  ( E. x  e.  _V  ph  <->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376   E.wex 1671    e. wcel 1904   E.wrex 2757   _Vcvv 3031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-rex 2762  df-v 3033
This theorem is referenced by:  rexcom4  3053  spesbc  3337  exopxfr  4983  dfco2  5341  dfco2a  5342  dffv2  5953  finacn  8499  ac6s2  8934  ptcmplem3  21147  ustn0  21313  hlimeui  26974  rexcom4f  28192  isrnsigaOLD  29008  isrnsiga  29009  prdstotbnd  32190  ac6s3f  32478  moxfr  35605  eldioph2b  35676  kelac1  35992  relintabex  36258  cbvexsv  36983
  Copyright terms: Public domain W3C validator