Theorem ceqsexv 2895

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)

Hypotheses

Ref	Expression
ceqsexv.1	⊢ A ∈ V
ceqsexv.2	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
ceqsexv	⊢ (∃x(x = A ∧ φ) ↔ ψ)

Distinct variable groups:   x,A   ψ,x

Allowed substitution hint:   φ(x)

Proof of Theorem ceqsexv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxψ
2		ceqsexv.1	. 2 ⊢ A ∈ V
3		ceqsexv.2	. 2 ⊢ (x = A → (φ ↔ ψ))
4	1, 2, 3	ceqsex 2894	1 ⊢ (∃x(x = A ∧ φ) ↔ ψ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2862

This theorem is referenced by:  ceqsex3v  2898  gencbvex  2902  sbhypf  2905  euxfr2  3022  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  eluni1g  4173  opkelcokg  4262  opkelimagekg  4272  dfimak2  4299  insklem  4305  ndisjrelk  4324  unipw1  4326  dfpw2  4328  dfaddc2  4382  dfnnc2  4396  elsuc  4414  addcass  4416  nnsucelrlem1  4425  ltfinex  4465  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspsslem1  4551  vfinspss  4552  vfinncsp  4555  dfop2lem1  4574  eqvinop  4607  el1st  4730  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  dfswap2  4742  dfid3  4769  opeliunxp  4821  elimapw1  4945  elimapw12  4946  elimapw13  4947  elimapw11c  4949  imai  5011  dmsnopg  5067  rnsnop  5076  coi1  5095  dfcnv2  5101  elxp4  5109  df2nd2  5112  iunfopab  5205  dmfco  5382  abrexco  5464  isomin  5497  opbr1st  5502  opbr2nd  5503  dfoprab2  5559  brsnsi1  5776  brsnsi2  5777  brco1st  5778  brco2nd  5779  trtxp  5782  elfix  5788  brimage  5794  oqelins4  5795  txpcofun  5804  otsnelsi3  5806  addcfnex  5825  funsex  5829  qrpprod  5837  pw1fnf1o  5856  clos1ex  5877  enex  6032  xpassenlem  6057  xpassen  6058  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  enpw1pw  6076  enprmaplem1  6077  ovmuc  6131  mucex  6134  ovcelem1  6172  ceexlem1  6174  ceex  6175  el2c  6192  taddc  6230  tcfnex  6245  csucex  6260  nnltp1clem1  6262  addccan2nclem1  6264  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  nnc3n3p1  6279  spacvallem1  6282  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305