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

Theorem ceqsexv 3237
 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 1841 . 2 𝑥𝜓
2 ceqsexv.1 . 2 𝐴 ∈ V
3 ceqsexv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsex 3236 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1481  ∃wex 1702   ∈ wcel 1988  Vcvv 3195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-12 2045  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-v 3197 This theorem is referenced by:  ceqsexv2d  3238  ceqsex3v  3241  gencbvex  3245  euxfr2  3385  inuni  4817  eqvinop  4945  elvvv  5168  dmfco  6259  fndmdif  6307  fndmin  6310  fmptco  6382  abrexco  6487  uniuni  6956  elxp4  7095  elxp5  7096  opabex3d  7130  opabex3  7131  fsplit  7267  brtpos2  7343  mapsnen  8020  xpsnen  8029  xpcomco  8035  xpassen  8039  dfac5lem1  8931  dfac5lem2  8932  dfac5lem3  8933  cf0  9058  ltexprlem4  9846  pceu  15532  4sqlem12  15641  vdwapun  15659  gsumval3eu  18286  dprd2d2  18424  znleval  19884  metrest  22310  fmptcof2  29430  fpwrelmapffslem  29481  dfdm5  31650  dfrn5  31651  elima4  31653  brtxp  31962  brpprod  31967  elfix  31985  dffix2  31987  sscoid  31995  elfuns  31997  dfiota3  32005  brimg  32019  brapply  32020  brsuccf  32023  funpartlem  32024  brrestrict  32031  dfrecs2  32032  dfrdg4  32033  lshpsmreu  34215  isopos  34286  islpln5  34640  islvol5  34684  pmapglb  34875  polval2N  35011  cdlemftr3  35672  dibelval3  36255  dicelval3  36288  mapdpglem3  36783  hdmapglem7a  37038  diophrex  37158  mapsnend  39207  opeliun2xp  41876
 Copyright terms: Public domain W3C validator