Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexv 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

Proof of Theorem rexv
StepHypRef Expression
1 df-rex 2813 . 2
2 vex 3112 . . . 4
32biantrur 506 . . 3
43exbii 1667 . 2
51, 4bitr4i 252 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808   cvv 3109 This theorem is referenced by:  rexcom4  3129  spesbc  3420  exopxfr  5151  dfco2  5511  dfco2a  5512  dffv2  5946  finacn  8452  ac6s2  8887  ptcmplem3  20554  ustn0  20723  hlimeui  26158  rexcom4f  27376  isrnsigaOLD  28112  isrnsiga  28113  prdstotbnd  30290  ac6s3f  30579  moxfr  30624  eldioph2b  30696  kelac1  31009  cbvexsv  33319 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-rex 2813  df-v 3111
 Copyright terms: Public domain W3C validator