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

Theorem ceqsexv 3394
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 1995 . 2 𝑥𝜓
2 ceqsexv.1 . 2 𝐴 ∈ V
3 ceqsexv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsex 3393 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  Vcvv 3351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353
This theorem is referenced by:  ceqsexv2d  3395  ceqsex3v  3398  gencbvex  3402  euxfr2  3543  inuni  4957  eqvinop  5082  elvvv  5318  dmfco  6414  fndmdif  6464  fndmin  6467  fmptco  6539  abrexco  6645  uniuni  7118  elxp4  7257  elxp5  7258  opabex3d  7292  opabex3  7293  fsplit  7433  brtpos2  7510  mapsnend  8188  xpsnen  8200  xpcomco  8206  xpassen  8210  dfac5lem1  9146  dfac5lem2  9147  dfac5lem3  9148  cf0  9275  ltexprlem4  10063  pceu  15758  4sqlem12  15867  vdwapun  15885  gsumval3eu  18512  dprd2d2  18651  znleval  20118  metrest  22549  fmptcof2  29797  fpwrelmapffslem  29847  dfdm5  32012  dfrn5  32013  elima4  32015  brtxp  32324  brpprod  32329  elfix  32347  dffix2  32349  sscoid  32357  dfiota3  32367  brimg  32381  brapply  32382  brsuccf  32385  funpartlem  32386  brrestrict  32393  dfrecs2  32394  dfrdg4  32395  lshpsmreu  34918  isopos  34989  islpln5  35343  islvol5  35387  pmapglb  35578  polval2N  35714  cdlemftr3  36374  dibelval3  36957  dicelval3  36990  mapdpglem3  37485  hdmapglem7a  37737  diophrex  37865  opeliun2xp  42639
  Copyright terms: Public domain W3C validator