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

Theorem ceqsexv 3546
 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 1908 . 2 𝑥𝜓
2 ceqsexv.1 . 2 𝐴 ∈ V
3 ceqsexv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsex 3545 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530  ∃wex 1773   ∈ wcel 2107  Vcvv 3499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-cleq 2818  df-clel 2897 This theorem is referenced by:  ceqsexv2d  3547  ceqsex2v  3549  ceqsex3v  3550  gencbvex  3554  euxfr2w  3714  euxfr2  3716  inuni  5242  eqvinop  5374  elvvv  5625  dmfco  6753  fndmdif  6807  fndmin  6810  fmptco  6886  abrexco  7000  uniuni  7476  elxp4  7618  elxp5  7619  brtpos2  7892  xpsnen  8593  xpcomco  8599  xpassen  8603  dfac5lem2  9542  cf0  9665  ltexprlem4  10453  pceu  16175  4sqlem12  16284  vdwapun  16302  gsumval3eu  18946  dprd2d2  19088  znleval  20617  metrest  23049  fmptcof2  30317  fpwrelmapffslem  30381  cusgredgex  32252  dfdm5  32900  dfrn5  32901  elima4  32903  brtxp  33225  brpprod  33230  elfix  33248  dfiota3  33268  brimg  33282  brapply  33283  brsuccf  33286  funpartlem  33287  brrestrict  33294  dfrecs2  33295  dfrdg4  33296  lshpsmreu  36112  isopos  36183  islpln5  36538  islvol5  36582  cdlemftr3  37568  dibelval3  38150  dicelval3  38183  mapdpglem3  38678  hdmapglem7a  38930  diophrex  39233
 Copyright terms: Public domain W3C validator