Theorem ceqsexv 3542

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 1841	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
2		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
3		ceqsexv.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	notbid 318	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
5	2, 4	ceqsalv 3529	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
6	1, 5	bitr3i 277	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ¬ 𝜓)
7	6	con4bii 321	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819

This theorem is referenced by:  ceqsexv2dOLD  3546  ceqsex2v  3548  ceqsex3v  3549  gencbvex  3553  euxfr2w  3742  euxfr2  3744  inuni  5368  eqvinop  5507  elvvv  5775  dmfco  7018  fndmdif  7075  fndmin  7078  fmptco  7163  abrexco  7281  imaeqsexvOLD  7399  imaeqexov  7688  uniuni  7797  elxp4  7962  elxp5  7963  brtpos2  8273  xpsnen  9121  xpcomco  9128  xpassen  9132  brttrcl2  9783  dfac5lem2  10193  cf0  10320  ltexprlem4  11108  pceu  16893  4sqlem12  17003  vdwapun  17021  gsumval3eu  19946  dprd2d2  20088  znleval  21596  metrest  24558  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  mulsuniflem  28193  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  renegscl  28448  readdscl  28449  remulscl  28452  fmptcof2  32675  fpwrelmapffslem  32746  cusgredgex  35089  dfdm5  35736  dfrn5  35737  elima4  35739  brtxp  35844  brpprod  35849  elfix  35867  dfiota3  35887  brimg  35901  brapply  35902  brsuccf  35905  funpartlem  35906  brrestrict  35913  dfrecs2  35914  dfrdg4  35915  lshpsmreu  39065  isopos  39136  islpln5  39492  islvol5  39536  cdlemftr3  40522  dibelval3  41104  dicelval3  41137  mapdpglem3  41632  hdmapglem7a  41884  diophrex  42731