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

Theorem rexv 3372
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 3067 . 2 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2 vex 3354 . . . 4 𝑥 ∈ V
32biantrur 516 . . 3 (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
43exbii 1924 . 2 (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
51, 4bitr4i 267 1 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  wex 1852  wcel 2145  wrex 3062  Vcvv 3351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-rex 3067  df-v 3353
This theorem is referenced by:  rexcom4  3377  spesbc  3671  exopxfr  5405  dfco2  5779  dfco2a  5780  dffv2  6414  abnex  7113  finacn  9074  ac6s2  9511  ptcmplem3  22079  ustn0  22245  hlimeui  28438  rexcom4f  29658  isrnsigaOLD  30516  isrnsiga  30517  prdstotbnd  33926  ac6s3f  34312  moxfr  37782  eldioph2b  37853  kelac1  38160  relintabex  38414  cbvexsv  39288  sprid  42253
  Copyright terms: Public domain W3C validator