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

Theorem rexv 3206
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 2913 . 2 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
2 vex 3189 . . . 4 𝑥 ∈ V
32biantrur 527 . . 3 (𝜑 ↔ (𝑥 ∈ V ∧ 𝜑))
43exbii 1771 . 2 (∃𝑥𝜑 ↔ ∃𝑥(𝑥 ∈ V ∧ 𝜑))
51, 4bitr4i 267 1 (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1701  wcel 1987  wrex 2908  Vcvv 3186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-rex 2913  df-v 3188
This theorem is referenced by:  rexcom4  3211  spesbc  3502  exopxfr  5225  dfco2  5593  dfco2a  5594  dffv2  6228  finacn  8817  ac6s2  9252  ptcmplem3  21768  ustn0  21934  hlimeui  27946  rexcom4f  29166  isrnsigaOLD  29956  isrnsiga  29957  prdstotbnd  33225  ac6s3f  33611  moxfr  36735  eldioph2b  36806  kelac1  37113  relintabex  37368  cbvexsv  38244  sprid  41012
  Copyright terms: Public domain W3C validator