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 1880	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 281	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  spesbc  3828  exopxfr  5820  elres  6008  elid  6193  dfco2  6246  dfco2a  6247  dffv2  6981  abnex  7772  finacn  10133  ac6s2  10568  ptcmplem3  24379  ustn0  24546  hlimeui  31848  rexcom4f  33113  isrnsiga  34792  onvf1odlem1  35951  onprcf1of1ord  35975  vsmrep  36010  prdstotbnd  38822  ac6s3f  39197  moxfr  43797  eldioph2b  43868  kelac1  44159  cbvexsv  45624  sprid  48650