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

Step	Hyp	Ref	Expression
1		nfv 1840	. 2 ⊢ Ⅎ𝑥𝜓
2		ceqsexv.1	. 2 ⊢ 𝐴 ∈ V
3		ceqsexv.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	ceqsex 3227	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

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