Theorem ceqsexv 3511

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 3500	. . 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 3459

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 2809

This theorem is referenced by:  ceqsexv2dOLD  3513  ceqsex2v  3515  ceqsex3v  3516  gencbvex  3520  euxfr2w  3703  euxfr2  3705  inuni  5320  eqvinop  5462  elvvv  5730  dmfco  6975  fndmdif  7032  fndmin  7035  fmptco  7119  abrexco  7236  imaeqsexvOLD  7356  imaeqexov  7645  uniuni  7756  elxp4  7918  elxp5  7919  brtpos2  8231  xpsnen  9069  xpcomco  9076  xpassen  9080  brttrcl2  9728  dfac5lem2  10138  cf0  10265  ltexprlem4  11053  pceu  16866  4sqlem12  16976  vdwapun  16994  gsumval3eu  19885  dprd2d2  20027  znleval  21515  metrest  24463  sleadd1  27948  addsuniflem  27960  addsasslem1  27962  addsasslem2  27963  mulsuniflem  28104  addsdilem1  28106  addsdilem2  28107  mulsasslem1  28118  mulsasslem2  28119  renegscl  28401  readdscl  28402  remulscl  28405  fmptcof2  32635  fpwrelmapffslem  32709  cusgredgex  35144  dfdm5  35790  dfrn5  35791  elima4  35793  brtxp  35898  brpprod  35903  elfix  35921  dfiota3  35941  brimg  35955  brapply  35956  brsuccf  35959  funpartlem  35960  brrestrict  35967  dfrecs2  35968  dfrdg4  35969  lshpsmreu  39127  isopos  39198  islpln5  39554  islvol5  39598  cdlemftr3  40584  dibelval3  41166  dicelval3  41199  mapdpglem3  41694  hdmapglem7a  41946  diophrex  42798