Theorem ceqsexv 3543

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 3542	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-cleq 2816  df-clel 2895

This theorem is referenced by:  ceqsexv2d  3544  ceqsex2v  3546  ceqsex3v  3547  gencbvex  3551  euxfr2w  3713  euxfr2  3715  inuni  5248  eqvinop  5380  elvvv  5629  dmfco  6759  fndmdif  6814  fndmin  6817  fmptco  6893  abrexco  7005  uniuni  7486  elxp4  7629  elxp5  7630  brtpos2  7900  xpsnen  8603  xpcomco  8609  xpassen  8613  dfac5lem2  9552  cf0  9675  ltexprlem4  10463  pceu  16185  4sqlem12  16294  vdwapun  16312  gsumval3eu  19026  dprd2d2  19168  znleval  20703  metrest  23136  fmptcof2  30404  fpwrelmapffslem  30470  cusgredgex  32370  dfdm5  33018  dfrn5  33019  elima4  33021  brtxp  33343  brpprod  33348  elfix  33366  dfiota3  33386  brimg  33400  brapply  33401  brsuccf  33404  funpartlem  33405  brrestrict  33412  dfrecs2  33413  dfrdg4  33414  lshpsmreu  36247  isopos  36318  islpln5  36673  islvol5  36717  cdlemftr3  37703  dibelval3  38285  dicelval3  38318  mapdpglem3  38813  hdmapglem7a  39065  diophrex  39379