MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexv Structured version   Visualization version   GIF version

Theorem rexv 3497
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
StepHypRef Expression
1 df-rex 3132 . 2 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2 vex 3474 . . . 4 𝑥 ∈ V
32biantrur 534 . . 3 (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
43exbii 1849 . 2 (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
51, 4bitr4i 281 1 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wex 1781  wcel 2115  wrex 3127  Vcvv 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-rex 3132  df-v 3473
This theorem is referenced by:  rexcom4OLD  3503  spesbc  3840  exopxfr  5687  elres  5864  elid  6029  dfco2  6071  dfco2a  6072  dffv2  6729  abnex  7454  finacn  9453  ac6s2  9885  ptcmplem3  22638  ustn0  22805  hlimeui  29002  rexcom4f  30219  isrnsiga  31380  prdstotbnd  35118  ac6s3f  35495  moxfr  39444  eldioph2b  39515  kelac1  39818  cbvexsv  41068  sprid  43814
  Copyright terms: Public domain W3C validator