Theorem ceqsexv 3491

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2185. (Revised by GG, 12-Oct-2024.) (Proof shortened by Wolf Lammen, 22-Jan-2025.)

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		alinexa 1845	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
2		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
3		ceqsexv.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	notbid 318	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
5	2, 4	ceqsalv 3481	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
6	1, 5	bitr3i 277	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ¬ 𝜓)
7	6	con4bii 321	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  ceqsexv2dOLD  3493  ceqsex2v  3495  ceqsex3v  3496  gencbvex  3500  euxfr2w  3679  euxfr2  3681  inuni  5296  eqvinop  5436  elvvv  5701  dmfco  6931  fndmdif  6989  fndmin  6992  fmptco  7076  abrexco  7192  imaeqsexvOLD  7311  imaeqexov  7598  uniuni  7709  elxp4  7866  elxp5  7867  brtpos2  8176  xpsnen  8993  xpcomco  8999  xpassen  9003  brttrcl2  9627  dfac5lem2  10038  cf0  10165  ltexprlem4  10954  pceu  16778  4sqlem12  16888  vdwapun  16906  gsumval3eu  19837  dprd2d2  19979  znleval  21513  metrest  24472  sleadd1  27971  addsuniflem  27983  addsasslem1  27985  addsasslem2  27986  mulsuniflem  28131  addsdilem1  28133  addsdilem2  28134  mulsasslem1  28145  mulsasslem2  28146  elreno2  28474  renegscl  28477  readdscl  28478  remulscl  28481  fmptcof2  32717  fpwrelmapffslem  32792  cusgredgex  35297  dfdm5  35948  dfrn5  35949  elima4  35951  brtxp  36053  brpprod  36058  elfix  36076  dfiota3  36096  brimg  36110  brapply  36111  lemsuccf  36114  funpartlem  36117  brrestrict  36124  dfrecs2  36125  dfrdg4  36126  lshpsmreu  39406  isopos  39477  islpln5  39832  islvol5  39876  cdlemftr3  40862  dibelval3  41444  dicelval3  41477  mapdpglem3  41972  hdmapglem7a  42224  diophrex  43053