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

Theorem rexv 3508
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 3070 . 2 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2 vex 3483 . . . 4 𝑥 ∈ V
32biantrur 530 . . 3 (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
43exbii 1847 . 2 (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
51, 4bitr4i 278 1 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1778  wcel 2107  wrex 3069  Vcvv 3479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rex 3070  df-v 3481
This theorem is referenced by:  spesbc  3881  exopxfr  5853  elres  6037  elid  6218  dfco2  6264  dfco2a  6265  dffv2  7003  abnex  7778  finacn  10091  ac6s2  10527  ptcmplem3  24063  ustn0  24230  hlimeui  31260  rexcom4f  32488  isrnsiga  34115  prdstotbnd  37802  ac6s3f  38179  moxfr  42708  eldioph2b  42779  kelac1  43080  cbvexsv  44572  sprid  47466
  Copyright terms: Public domain W3C validator