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

Theorem ceqsexv 3346
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 1956 . 2 𝑥𝜓
2 ceqsexv.1 . 2 𝐴 ∈ V
3 ceqsexv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsex 3345 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wex 1817  wcel 2103  Vcvv 3304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-12 2160  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-v 3306
This theorem is referenced by:  ceqsexv2d  3347  ceqsex3v  3350  gencbvex  3354  euxfr2  3497  inuni  4931  eqvinop  5059  elvvv  5287  dmfco  6386  fndmdif  6436  fndmin  6439  fmptco  6511  abrexco  6617  uniuni  7088  elxp4  7227  elxp5  7228  opabex3d  7262  opabex3  7263  fsplit  7402  brtpos2  7478  mapsnen  8151  xpsnen  8160  xpcomco  8166  xpassen  8170  dfac5lem1  9059  dfac5lem2  9060  dfac5lem3  9061  cf0  9186  ltexprlem4  9974  pceu  15674  4sqlem12  15783  vdwapun  15801  gsumval3eu  18426  dprd2d2  18564  znleval  20026  metrest  22451  fmptcof2  29687  fpwrelmapffslem  29737  dfdm5  31902  dfrn5  31903  elima4  31905  brtxp  32214  brpprod  32219  elfix  32237  dffix2  32239  sscoid  32247  dfiota3  32257  brimg  32271  brapply  32272  brsuccf  32275  funpartlem  32276  brrestrict  32283  dfrecs2  32284  dfrdg4  32285  lshpsmreu  34816  isopos  34887  islpln5  35241  islvol5  35285  pmapglb  35476  polval2N  35612  cdlemftr3  36272  dibelval3  36855  dicelval3  36888  mapdpglem3  37383  hdmapglem7a  37638  diophrex  37758  mapsnend  39807  opeliun2xp  42538
  Copyright terms: Public domain W3C validator