Theorem ceqsexv 3489

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 1915	. 2 ⊢ Ⅎ𝑥𝜓
2		ceqsexv.1	. 2 ⊢ 𝐴 ∈ V
3		ceqsexv.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	ceqsex 3488	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870

This theorem is referenced by:  ceqsexv2d  3490  ceqsex2v  3492  ceqsex3v  3493  gencbvex  3497  euxfr2w  3659  euxfr2  3661  inuni  5210  eqvinop  5343  elvvv  5591  dmfco  6734  fndmdif  6789  fndmin  6792  fmptco  6868  abrexco  6981  uniuni  7464  elxp4  7609  elxp5  7610  brtpos2  7881  xpsnen  8584  xpcomco  8590  xpassen  8594  dfac5lem2  9535  cf0  9662  ltexprlem4  10450  pceu  16173  4sqlem12  16282  vdwapun  16300  gsumval3eu  19017  dprd2d2  19159  znleval  20246  metrest  23131  fmptcof2  30420  fpwrelmapffslem  30494  cusgredgex  32481  dfdm5  33129  dfrn5  33130  elima4  33132  brtxp  33454  brpprod  33459  elfix  33477  dfiota3  33497  brimg  33511  brapply  33512  brsuccf  33515  funpartlem  33516  brrestrict  33523  dfrecs2  33524  dfrdg4  33525  lshpsmreu  36405  isopos  36476  islpln5  36831  islvol5  36875  cdlemftr3  37861  dibelval3  38443  dicelval3  38476  mapdpglem3  38971  hdmapglem7a  39223  diophrex  39716