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

Proof of Theorem rexv
StepHypRef Expression
1 df-rex 2713 . 2
2 vex 2961 . . . 4
32biantrur 494 . . 3
43exbii 1593 . 2
51, 4bitr4i 245 1
 Colors of variables: wff set class Syntax hints:   wb 178   wa 360  wex 1551   wcel 1726  wrex 2708  cvv 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