Theorem ceqsexv 3479

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 3470	. . 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 3430

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  3481  ceqsex2v  3483  ceqsex3v  3484  gencbvex  3488  euxfr2w  3667  euxfr2  3669  inuni  5285  eqvinop  5433  elvvv  5698  dmfco  6928  fndmdif  6986  fndmin  6989  fmptco  7074  abrexco  7190  imaeqsexvOLD  7309  imaeqexov  7596  uniuni  7707  elxp4  7864  elxp5  7865  brtpos2  8173  xpsnen  8990  xpcomco  8996  xpassen  9000  brttrcl2  9624  dfac5lem2  10035  cf0  10162  ltexprlem4  10951  pceu  16775  4sqlem12  16885  vdwapun  16903  gsumval3eu  19837  dprd2d2  19979  znleval  21511  metrest  24467  leadds1  27969  addsuniflem  27981  addsasslem1  27983  addsasslem2  27984  mulsuniflem  28129  addsdilem1  28131  addsdilem2  28132  mulsasslem1  28143  mulsasslem2  28144  elreno2  28475  renegscl  28478  readdscl  28479  remulscl  28482  fmptcof2  32719  fpwrelmapffslem  32794  cusgredgex  35310  dfdm5  35961  dfrn5  35962  elima4  35964  brtxp  36066  brpprod  36071  elfix  36089  dfiota3  36109  brimg  36123  brapply  36124  lemsuccf  36127  funpartlem  36130  brrestrict  36137  dfrecs2  36138  dfrdg4  36139  lshpsmreu  39546  isopos  39617  islpln5  39972  islvol5  40016  cdlemftr3  41002  dibelval3  41584  dicelval3  41617  mapdpglem3  42112  hdmapglem7a  42364  diophrex  43206