Theorem ceqsexv 3532

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2177. (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 1843	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
2		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
3		ceqsexv.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	notbid 318	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
5	2, 4	ceqsalv 3521	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
6	1, 5	bitr3i 277	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ¬ 𝜓)
7	6	con4bii 321	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816

This theorem is referenced by:  ceqsexv2dOLD  3534  ceqsex2v  3536  ceqsex3v  3537  gencbvex  3541  euxfr2w  3726  euxfr2  3728  inuni  5350  eqvinop  5492  elvvv  5761  dmfco  7005  fndmdif  7062  fndmin  7065  fmptco  7149  abrexco  7264  imaeqsexvOLD  7383  imaeqexov  7671  uniuni  7782  elxp4  7944  elxp5  7945  brtpos2  8257  xpsnen  9095  xpcomco  9102  xpassen  9106  brttrcl2  9754  dfac5lem2  10164  cf0  10291  ltexprlem4  11079  pceu  16884  4sqlem12  16994  vdwapun  17012  gsumval3eu  19922  dprd2d2  20064  znleval  21573  metrest  24537  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  mulsuniflem  28175  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  renegscl  28430  readdscl  28431  remulscl  28434  fmptcof2  32667  fpwrelmapffslem  32743  cusgredgex  35127  dfdm5  35773  dfrn5  35774  elima4  35776  brtxp  35881  brpprod  35886  elfix  35904  dfiota3  35924  brimg  35938  brapply  35939  brsuccf  35942  funpartlem  35943  brrestrict  35950  dfrecs2  35951  dfrdg4  35952  lshpsmreu  39110  isopos  39181  islpln5  39537  islvol5  39581  cdlemftr3  40567  dibelval3  41149  dicelval3  41182  mapdpglem3  41677  hdmapglem7a  41929  diophrex  42786