Theorem ceqsexv 3481

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2191. (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 1851	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
2		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
3		ceqsexv.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	notbid 320	. . . 4 ⊢ (𝑥 = 𝐴 → (¬ 𝜑 ↔ ¬ 𝜓))
5	2, 4	ceqsalv 3472	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → ¬ 𝜑) ↔ ¬ 𝜓)
6	1, 5	bitr3i 279	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ¬ 𝜓)
7	6	con4bii 323	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 397  ∀wal 1546   = wceq 1548  ∃wex 1787   ∈ wcel 2121  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-clel 2816

This theorem is referenced by:  ceqsexv2dOLD  3483  ceqsex2v  3485  ceqsex3v  3486  gencbvex  3490  euxfr2w  3663  euxfr2  3665  inuni  5281  eqvinop  5430  elvvv  5697  dmfco  6927  fndmdif  6987  fndmin  6990  fmptco  7075  abrexco  7192  imaeqsexvOLD  7311  imaeqexov  7598  uniuni  7709  elxp4  7866  elxp5  7867  brtpos2  8176  xpsnen  8993  xpcomco  8999  xpassen  9003  brttrcl2  9630  dfac5lem2  10041  cf0  10168  ltexprlem4  10957  pceu  16812  4sqlem12  16922  vdwapun  16940  gsumval3eu  19874  dprd2d2  20016  znleval  21533  metrest  24511  leadds1  28003  addsuniflem  28015  addsasslem1  28017  addsasslem2  28018  mulsuniflem  28163  addsdilem1  28165  addsdilem2  28166  mulsasslem1  28177  mulsasslem2  28178  elreno2  28509  renegscl  28512  readdscl  28513  remulscl  28516  fmptcof2  32753  fpwrelmapffslem  32828  cusgredgex  35365  dfdm5  36016  dfrn5  36017  elima4  36019  brtxp  36121  brpprod  36126  elfix  36144  dfiota3  36164  brimg  36178  brapply  36179  lemsuccf  36182  funpartlem  36185  brrestrict  36192  dfrecs2  36193  dfrdg4  36194  lshpsmreu  39616  isopos  39687  islpln5  40042  islvol5  40086  cdlemftr3  41072  dibelval3  41654  dicelval3  41687  mapdpglem3  42182  hdmapglem7a  42434  diophrex  43239