Theorem ceqsexv 3501

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 3490	. . 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 3450

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 2804

This theorem is referenced by:  ceqsexv2dOLD  3503  ceqsex2v  3505  ceqsex3v  3506  gencbvex  3510  euxfr2w  3694  euxfr2  3696  inuni  5308  eqvinop  5450  elvvv  5717  dmfco  6960  fndmdif  7017  fndmin  7020  fmptco  7104  abrexco  7221  imaeqsexvOLD  7341  imaeqexov  7630  uniuni  7741  elxp4  7901  elxp5  7902  brtpos2  8214  xpsnen  9029  xpcomco  9036  xpassen  9040  brttrcl2  9674  dfac5lem2  10084  cf0  10211  ltexprlem4  10999  pceu  16824  4sqlem12  16934  vdwapun  16952  gsumval3eu  19841  dprd2d2  19983  znleval  21471  metrest  24419  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  mulsuniflem  28059  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  renegscl  28356  readdscl  28357  remulscl  28360  fmptcof2  32588  fpwrelmapffslem  32662  cusgredgex  35116  dfdm5  35767  dfrn5  35768  elima4  35770  brtxp  35875  brpprod  35880  elfix  35898  dfiota3  35918  brimg  35932  brapply  35933  brsuccf  35936  funpartlem  35937  brrestrict  35944  dfrecs2  35945  dfrdg4  35946  lshpsmreu  39109  isopos  39180  islpln5  39536  islvol5  39580  cdlemftr3  40566  dibelval3  41148  dicelval3  41181  mapdpglem3  41676  hdmapglem7a  41928  diophrex  42770