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

Theorem rexv 3251
 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 2947 . 2 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2 vex 3234 . . . 4 𝑥 ∈ V
32biantrur 526 . . 3 (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
43exbii 1814 . 2 (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
51, 4bitr4i 267 1 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1744   ∈ wcel 2030  ∃wrex 2942  Vcvv 3231 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-rex 2947  df-v 3233 This theorem is referenced by:  rexcom4  3256  spesbc  3554  exopxfr  5298  dfco2  5672  dfco2a  5673  dffv2  6310  abnex  7007  finacn  8911  ac6s2  9346  ptcmplem3  21905  ustn0  22071  hlimeui  28225  rexcom4f  29445  isrnsigaOLD  30303  isrnsiga  30304  prdstotbnd  33723  ac6s3f  34109  moxfr  37572  eldioph2b  37643  kelac1  37950  relintabex  38204  cbvexsv  39079  sprid  42049
 Copyright terms: Public domain W3C validator