Theorem ceqsexv 3529

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813

This theorem is referenced by:  ceqsexv2dOLD  3533  ceqsex2v  3535  ceqsex3v  3536  gencbvex  3540  euxfr2w  3728  euxfr2  3730  inuni  5355  eqvinop  5497  elvvv  5763  dmfco  7004  fndmdif  7061  fndmin  7064  fmptco  7148  abrexco  7263  imaeqsexvOLD  7382  imaeqexov  7670  uniuni  7780  elxp4  7944  elxp5  7945  brtpos2  8255  xpsnen  9093  xpcomco  9100  xpassen  9104  brttrcl2  9751  dfac5lem2  10161  cf0  10288  ltexprlem4  11076  pceu  16879  4sqlem12  16989  vdwapun  17007  gsumval3eu  19936  dprd2d2  20078  znleval  21590  metrest  24552  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  mulsuniflem  28189  addsdilem1  28191  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  renegscl  28444  readdscl  28445  remulscl  28448  fmptcof2  32673  fpwrelmapffslem  32749  cusgredgex  35105  dfdm5  35753  dfrn5  35754  elima4  35756  brtxp  35861  brpprod  35866  elfix  35884  dfiota3  35904  brimg  35918  brapply  35919  brsuccf  35922  funpartlem  35923  brrestrict  35930  dfrecs2  35931  dfrdg4  35932  lshpsmreu  39090  isopos  39161  islpln5  39517  islvol5  39561  cdlemftr3  40547  dibelval3  41129  dicelval3  41162  mapdpglem3  41657  hdmapglem7a  41909  diophrex  42762