Theorem rexv 3480

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 3086	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3457	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantrur 538	. . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
4	3	exbii 1867	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 280	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-v 3455

This theorem is referenced by:  spesbc  3833  exopxfr  5811  elres  6002  elid  6181  dfco2  6227  dfco2a  6228  dffv2  6957  abnex  7735  finacn  10000  ac6s2  10437  ptcmplem3  24102  ustn0  24269  hlimeui  31400  rexcom4f  32626  isrnsiga  34371  onvf1odlem1  35407  prdstotbnd  38254  ac6s3f  38631  moxfr  43234  eldioph2b  43305  kelac1  43601  cbvexsv  45084  sprid  48041