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

Theorem ceqsexv 3228
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
Hypotheses
Ref Expression
ceqsexv.1 𝐴 ∈ V
ceqsexv.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ceqsexv (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ceqsexv
StepHypRef Expression
1 nfv 1840 . 2 𝑥𝜓
2 ceqsexv.1 . 2 𝐴 ∈ V
3 ceqsexv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsex 3227 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  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-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3188
This theorem is referenced by:  ceqsexv2d  3229  ceqsex3v  3232  gencbvex  3236  euxfr2  3373  inuni  4786  eqvinop  4915  elvvv  5139  dmfco  6229  fndmdif  6277  fndmin  6280  fmptco  6351  abrexco  6456  uniuni  6920  elxp4  7057  elxp5  7058  opabex3d  7091  opabex3  7092  fsplit  7227  brtpos2  7303  mapsnen  7979  xpsnen  7988  xpcomco  7994  xpassen  7998  dfac5lem1  8890  dfac5lem2  8891  dfac5lem3  8892  cf0  9017  ltexprlem4  9805  pceu  15475  4sqlem12  15584  vdwapun  15602  gsumval3eu  18226  dprd2d2  18364  znleval  19822  metrest  22239  fmptcof2  29296  fpwrelmapffslem  29347  dfdm5  31375  dfrn5  31376  elima4  31378  brtxp  31626  brpprod  31631  elfix  31649  dffix2  31651  sscoid  31659  elfuns  31661  dfiota3  31669  brimg  31683  brapply  31684  brsuccf  31687  funpartlem  31688  brrestrict  31695  dfrecs2  31696  dfrdg4  31697  lshpsmreu  33873  isopos  33944  islpln5  34298  islvol5  34342  pmapglb  34533  polval2N  34669  cdlemftr3  35330  dibelval3  35913  dicelval3  35946  mapdpglem3  36441  hdmapglem7a  36696  diophrex  36816  mapsnend  38862  opeliun2xp  41396
  Copyright terms: Public domain W3C validator