Theorem ceqsexv 3215

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  ceqsexv2d  3216  ceqsex3v  3219  gencbvex  3223  euxfr2  3358  inuni  4753  eqvinop  4881  elvvv  5101  dmfco  6182  fndmdif  6229  fndmin  6232  fmptco  6303  abrexco  6406  uniuni  6865  elxp4  7003  elxp5  7004  opabex3d  7037  opabex3  7038  fsplit  7169  brtpos2  7245  mapsnen  7920  xpsnen  7929  xpcomco  7935  xpassen  7939  dfac5lem1  8829  dfac5lem2  8830  dfac5lem3  8831  cf0  8956  ltexprlem4  9740  pceu  15389  4sqlem12  15498  vdwapun  15516  gsumval3eu  18128  dprd2d2  18266  znleval  19722  metrest  22139  fmptcof2  28839  fpwrelmapffslem  28895  dfdm5  30921  dfrn5  30922  elima4  30924  nofulllem5  31105  brtxp  31157  brpprod  31162  elfix  31180  dffix2  31182  sscoid  31190  elfuns  31192  dfiota3  31200  brimg  31214  brapply  31215  brsuccf  31218  funpartlem  31219  brrestrict  31226  dfrecs2  31227  dfrdg4  31228  lshpsmreu  33414  isopos  33485  islpln5  33839  islvol5  33883  pmapglb  34074  polval2N  34210  cdlemftr3  34871  dibelval3  35454  dicelval3  35487  mapdpglem3  35982  hdmapglem7a  36237  diophrex  36357  mapsnend  38386  opeliun2xp  41904