Theorem ceqsexv 3498

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2178. (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 3487	. . 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 2109  Vcvv 3447

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 2008  ax-8 2111

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

This theorem is referenced by:  ceqsexv2dOLD  3500  ceqsex2v  3502  ceqsex3v  3503  gencbvex  3507  euxfr2w  3691  euxfr2  3693  inuni  5305  eqvinop  5447  elvvv  5714  dmfco  6957  fndmdif  7014  fndmin  7017  fmptco  7101  abrexco  7218  imaeqsexvOLD  7338  imaeqexov  7627  uniuni  7738  elxp4  7898  elxp5  7899  brtpos2  8211  xpsnen  9025  xpcomco  9031  xpassen  9035  brttrcl2  9667  dfac5lem2  10077  cf0  10204  ltexprlem4  10992  pceu  16817  4sqlem12  16927  vdwapun  16945  gsumval3eu  19834  dprd2d2  19976  znleval  21464  metrest  24412  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  mulsuniflem  28052  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  renegscl  28349  readdscl  28350  remulscl  28353  fmptcof2  32581  fpwrelmapffslem  32655  cusgredgex  35109  dfdm5  35760  dfrn5  35761  elima4  35763  brtxp  35868  brpprod  35873  elfix  35891  dfiota3  35911  brimg  35925  brapply  35926  brsuccf  35929  funpartlem  35930  brrestrict  35937  dfrecs2  35938  dfrdg4  35939  lshpsmreu  39102  isopos  39173  islpln5  39529  islvol5  39573  cdlemftr3  40559  dibelval3  41141  dicelval3  41174  mapdpglem3  41669  hdmapglem7a  41921  diophrex  42763