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  7126  abrexco  7242  imaeqsexv  7359  imaeqexov  7644  uniuni  7748  elxp4  7912  elxp5  7913  brtpos2  8216  xpsnen  9054  xpcomco  9061  xpassen  9065  brttrcl2  9708  dfac5lem2  10118  cf0  10245  ltexprlem4  11033  pceu  16778  4sqlem12  16888  vdwapun  16906  gsumval3eu  19771  dprd2d2  19913  znleval  21109  metrest  24032  sleadd1  27469  addsuniflem  27481  addsasslem1  27483  addsasslem2  27484  mulsuniflem  27601  addsdilem1  27603  addsdilem2  27604  mulsasslem1  27615  mulsasslem2  27616  fmptcof2  31877  fpwrelmapffslem  31952  cusgredgex  34107  dfdm5  34739  dfrn5  34740  elima4  34742  brtxp  34847  brpprod  34852  elfix  34870  dfiota3  34890  brimg  34904  brapply  34905  brsuccf  34908  funpartlem  34909  brrestrict  34916  dfrecs2  34917  dfrdg4  34918  lshpsmreu  37974  isopos  38045  islpln5  38401  islvol5  38445  cdlemftr3  39431  dibelval3  40013  dicelval3  40046  mapdpglem3  40541  hdmapglem7a  40793  diophrex  41503