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

Theorem rexv 2972
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 2713 . 2  |-  ( E. x  e.  _V  ph  <->  E. x ( x  e. 
_V  /\  ph ) )
2 vex 2961 . . . 4  |-  x  e. 
_V
32biantrur 494 . . 3  |-  ( ph  <->  ( x  e.  _V  /\  ph ) )
43exbii 1593 . 2  |-  ( E. x ph  <->  E. x
( x  e.  _V  /\ 
ph ) )
51, 4bitr4i 245 1  |-  ( E. x  e.  _V  ph  <->  E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1551    e. wcel 1726   E.wrex 2708   _Vcvv 2958
This theorem is referenced by:  rexcom4  2977  spesbc  3244  dfco2  5372  dfco2a  5373  dffv2  5799  exopxfr  6413  finacn  7936  ac6s2  8371  ptcmplem3  18090  ustn0  18255  hlimeui  22748  rexcom4f  23971  isrnsigaOLD  24500  isrnsiga  24501  prdstotbnd  26517  moxfr  26747  eldioph2b  26835  kelac1  27152  cbvexsv  28707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-rex 2713  df-v 2960
  Copyright terms: Public domain W3C validator