Theorem rexv 3467

Description: An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)

Assertion

Ref	Expression
rexv	⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

Proof of Theorem rexv

Step	Hyp	Ref	Expression
1		df-rex 3112	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3444	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantrur 534	. . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
4	3	exbii 1849	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 281	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rex 3112  df-v 3443

This theorem is referenced by:  rexcom4OLD  3473  spesbc  3811  exopxfr  5678  elres  5857  elid  6023  dfco2  6065  dfco2a  6066  dffv2  6733  abnex  7459  finacn  9461  ac6s2  9897  ptcmplem3  22659  ustn0  22826  hlimeui  29023  rexcom4f  30241  isrnsiga  31482  prdstotbnd  35232  ac6s3f  35609  moxfr  39633  eldioph2b  39704  kelac1  40007  cbvexsv  41253  sprid  43991