Theorem ceqsexv 3525

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2171. (Revised by Gino Giotto, 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 317	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
5	2, 4	ceqsalv 3511	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
6	1, 5	bitr3i 276	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ¬ 𝜓)
7	6	con4bii 320	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  Vcvv 3474

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 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2810

This theorem is referenced by:  ceqsexv2d  3528  ceqsex2v  3530  ceqsex3v  3531  gencbvex  3535  euxfr2w  3716  euxfr2  3718  inuni  5343  eqvinop  5487  elvvv  5751  dmfco  6987  fndmdif  7043  fndmin  7046  fmptco  7129  abrexco  7245  imaeqsexv  7362  imaeqexov  7647  uniuni  7751  elxp4  7915  elxp5  7916  brtpos2  8219  xpsnen  9057  xpcomco  9064  xpassen  9068  brttrcl2  9711  dfac5lem2  10121  cf0  10248  ltexprlem4  11036  pceu  16781  4sqlem12  16891  vdwapun  16909  gsumval3eu  19774  dprd2d2  19916  znleval  21116  metrest  24040  sleadd1  27482  addsuniflem  27494  addsasslem1  27496  addsasslem2  27497  mulsuniflem  27614  addsdilem1  27616  addsdilem2  27617  mulsasslem1  27628  mulsasslem2  27629  fmptcof2  31920  fpwrelmapffslem  31995  cusgredgex  34181  dfdm5  34813  dfrn5  34814  elima4  34816  brtxp  34921  brpprod  34926  elfix  34944  dfiota3  34964  brimg  34978  brapply  34979  brsuccf  34982  funpartlem  34983  brrestrict  34990  dfrecs2  34991  dfrdg4  34992  lshpsmreu  38065  isopos  38136  islpln5  38492  islvol5  38536  cdlemftr3  39522  dibelval3  40104  dicelval3  40137  mapdpglem3  40632  hdmapglem7a  40884  diophrex  41595