Theorem rexv 3490

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 3096	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3467	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantrur 539	. . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
4	3	exbii 1875	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 281	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-v 3465

This theorem is referenced by:  spesbc  3844  exopxfr  5827  elres  6017  elid  6197  dfco2  6243  dfco2a  6244  dffv2  6974  abnex  7752  finacn  10030  ac6s2  10466  ptcmplem3  24176  ustn0  24343  hlimeui  31529  rexcom4f  32752  isrnsiga  34444  onvf1odlem1  35482  prdstotbnd  38328  ac6s3f  38705  moxfr  43308  eldioph2b  43379  kelac1  43675  cbvexsv  45141  sprid  48105