Theorem rexv 3484

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 3092	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3461	. . . 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 2146  ∃wrex 3091  Vcvv 3457

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-v 3459

This theorem is used by:  spesbc  3836  exopxfr  5831  elres  6021  elid  6200  dfco2  6248  dfco2a  6249  dffv2  6980  abnex  7758  finacn  10046  ac6s2  10481  ptcmplem3  24240  ustn0  24407  hlimeui  31621  rexcom4f  32844  isrnsiga  34526  onvf1odlem1  35603  prdstotbnd  38478  ac6s3f  38853  moxfr  43456  eldioph2b  43527  kelac1  43823  cbvexsv  45289  sprid  48256