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

Step	Hyp	Ref	Expression
1		df-rex 2813	. 2
2		vex 3112	. . . 4
3	2	biantrur 506	. . 3
4	3	exbii 1667	. 2
5	1, 4	bitr4i 252	1

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