Theorem rexv 3466

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 3054	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3442	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantrur 530	. . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
4	3	exbii 1848	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 278	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3440

This theorem is referenced by:  spesbc  3836  exopxfr  5790  elres  5975  elid  6152  dfco2  6198  dfco2a  6199  dffv2  6922  abnex  7697  finacn  9963  ac6s2  10399  ptcmplem3  23957  ustn0  24124  hlimeui  31202  rexcom4f  32430  isrnsiga  34082  onvf1odlem1  35078  prdstotbnd  37776  ac6s3f  38153  moxfr  42668  eldioph2b  42739  kelac1  43039  cbvexsv  44524  sprid  47462