Theorem ceqsexv 3346

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1596  ∃wex 1817   ∈ wcel 2103  Vcvv 3304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-12 2160  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-v 3306

This theorem is referenced by:  ceqsexv2d  3347  ceqsex3v  3350  gencbvex  3354  euxfr2  3497  inuni  4931  eqvinop  5059  elvvv  5287  dmfco  6386  fndmdif  6436  fndmin  6439  fmptco  6511  abrexco  6617  uniuni  7088  elxp4  7227  elxp5  7228  opabex3d  7262  opabex3  7263  fsplit  7402  brtpos2  7478  mapsnen  8151  xpsnen  8160  xpcomco  8166  xpassen  8170  dfac5lem1  9059  dfac5lem2  9060  dfac5lem3  9061  cf0  9186  ltexprlem4  9974  pceu  15674  4sqlem12  15783  vdwapun  15801  gsumval3eu  18426  dprd2d2  18564  znleval  20026  metrest  22451  fmptcof2  29687  fpwrelmapffslem  29737  dfdm5  31902  dfrn5  31903  elima4  31905  brtxp  32214  brpprod  32219  elfix  32237  dffix2  32239  sscoid  32247  dfiota3  32257  brimg  32271  brapply  32272  brsuccf  32275  funpartlem  32276  brrestrict  32283  dfrecs2  32284  dfrdg4  32285  lshpsmreu  34816  isopos  34887  islpln5  35241  islvol5  35285  pmapglb  35476  polval2N  35612  cdlemftr3  36272  dibelval3  36855  dicelval3  36888  mapdpglem3  37383  hdmapglem7a  37638  diophrex  37758  mapsnend  39807  opeliun2xp  42538