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 3072	. 2 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2		vex 3445	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantrur 531	. . 3 ⊢ (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
4	3	exbii 1849	. 2 ⊢ (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
5	1, 4	bitr4i 277	1 ⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1780   ∈ wcel 2105  ∃wrex 3071  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3072  df-v 3443

This theorem is referenced by:  spesbc  3825  exopxfr  5773  elres  5950  elid  6125  dfco2  6171  dfco2a  6172  dffv2  6903  abnex  7649  finacn  9886  ac6s2  10322  ptcmplem3  23288  ustn0  23455  hlimeui  29738  rexcom4f  30955  isrnsiga  32221  prdstotbnd  36024  ac6s3f  36401  moxfr  40730  eldioph2b  40801  kelac1  41105  cbvexsv  42401  sprid  45191