Theorem rexv 3477

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 3087	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantrur 540	. . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
4	3	exbii 1881	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 281	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452

This theorem is used by:  spesbc  3829  exopxfr  5823  elres  6013  elid  6193  dfco2  6241  dfco2a  6242  dffv2  6973  abnex  7756  finacn  10053  ac6s2  10488  ptcmplem3  24280  ustn0  24447  hlimeui  31721  rexcom4f  32944  isrnsiga  34623  onvf1odlem1  35700  prdstotbnd  38544  ac6s3f  38919  moxfr  43537  eldioph2b  43608  kelac1  43904  cbvexsv  45370  sprid  48374