Theorem ceqsexv 3428

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   = wceq 1653  ∃wex 1875   ∈ wcel 2157  Vcvv 3383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-v 3385

This theorem is referenced by:  ceqsexv2d  3429  ceqsex3v  3432  gencbvex  3436  euxfr2  3585  inuni  5016  eqvinop  5143  elvvv  5379  dmfco  6495  fndmdif  6545  fndmin  6548  fmptco  6621  abrexco  6728  uniuni  7202  elxp4  7343  elxp5  7344  opabex3d  7377  opabex3  7378  brtpos2  7594  mapsnend  8272  xpsnen  8284  xpcomco  8290  xpassen  8294  dfac5lem1  9230  dfac5lem2  9231  dfac5lem3  9232  cf0  9359  ltexprlem4  10147  pceu  15880  4sqlem12  15989  vdwapun  16007  gsumval3eu  18616  dprd2d2  18755  znleval  20220  metrest  22653  fmptcof2  29967  fpwrelmapffslem  30016  dfdm5  32179  dfrn5  32180  elima4  32182  brtxp  32491  brpprod  32496  elfix  32514  dffix2  32516  sscoid  32524  dfiota3  32534  brimg  32548  brapply  32549  brsuccf  32552  funpartlem  32553  brrestrict  32560  dfrecs2  32561  dfrdg4  32562  lshpsmreu  35121  isopos  35192  islpln5  35547  islvol5  35591  pmapglb  35782  polval2N  35918  cdlemftr3  36577  dibelval3  37159  dicelval3  37192  mapdpglem3  37687  hdmapglem7a  37939  diophrex  38112  opeliun2xp  42897