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

Theorem rexv 3193
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 2902 . 2 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2 vex 3176 . . . 4 𝑥 ∈ V
32biantrur 526 . . 3 (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
43exbii 1764 . 2 (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
51, 4bitr4i 266 1 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  wex 1695  wcel 1977  wrex 2897  Vcvv 3173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rex 2902  df-v 3175
This theorem is referenced by:  rexcom4  3198  spesbc  3487  exopxfr  5187  dfco2  5551  dfco2a  5552  dffv2  6181  finacn  8756  ac6s2  9191  ptcmplem3  21668  ustn0  21834  hlimeui  27481  rexcom4f  28701  isrnsigaOLD  29502  isrnsiga  29503  prdstotbnd  32763  ac6s3f  33149  moxfr  36273  eldioph2b  36344  kelac1  36651  relintabex  36906  cbvexsv  37783
  Copyright terms: Public domain W3C validator