Theorem ceqsexv 3541

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

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

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 2793

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

This theorem is referenced by:  ceqsexv2d  3542  ceqsex2v  3544  ceqsex3v  3545  gencbvex  3549  euxfr2w  3711  euxfr2  3713  inuni  5246  eqvinop  5378  elvvv  5627  dmfco  6757  fndmdif  6812  fndmin  6815  fmptco  6891  abrexco  7003  uniuni  7484  elxp4  7627  elxp5  7628  brtpos2  7898  xpsnen  8601  xpcomco  8607  xpassen  8611  dfac5lem2  9550  cf0  9673  ltexprlem4  10461  pceu  16183  4sqlem12  16292  vdwapun  16310  gsumval3eu  19024  dprd2d2  19166  znleval  20701  metrest  23134  fmptcof2  30402  fpwrelmapffslem  30468  cusgredgex  32368  dfdm5  33016  dfrn5  33017  elima4  33019  brtxp  33341  brpprod  33346  elfix  33364  dfiota3  33384  brimg  33398  brapply  33399  brsuccf  33402  funpartlem  33403  brrestrict  33410  dfrecs2  33411  dfrdg4  33412  lshpsmreu  36260  isopos  36331  islpln5  36686  islvol5  36730  cdlemftr3  37716  dibelval3  38298  dicelval3  38331  mapdpglem3  38826  hdmapglem7a  39078  diophrex  39392