Theorem rexv 3251

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 2947	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3234	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantrur 526	. . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
4	3	exbii 1814	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 267	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1744   ∈ wcel 2030  ∃wrex 2942  Vcvv 3231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-rex 2947  df-v 3233

This theorem is referenced by:  rexcom4  3256  spesbc  3554  exopxfr  5298  dfco2  5672  dfco2a  5673  dffv2  6310  abnex  7007  finacn  8911  ac6s2  9346  ptcmplem3  21905  ustn0  22071  hlimeui  28225  rexcom4f  29445  isrnsigaOLD  30303  isrnsiga  30304  prdstotbnd  33723  ac6s3f  34109  moxfr  37572  eldioph2b  37643  kelac1  37950  relintabex  38204  cbvexsv  39079  sprid  42049