Theorem ceqsexv 3526

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811

This theorem is referenced by:  ceqsexv2d  3529  ceqsex2v  3531  ceqsex3v  3532  gencbvex  3536  euxfr2w  3717  euxfr2  3719  inuni  5344  eqvinop  5488  elvvv  5752  dmfco  6988  fndmdif  7044  fndmin  7047  fmptco  7127  abrexco  7243  imaeqsexv  7360  imaeqexov  7645  uniuni  7749  elxp4  7913  elxp5  7914  brtpos2  8217  xpsnen  9055  xpcomco  9062  xpassen  9066  brttrcl2  9709  dfac5lem2  10119  cf0  10246  ltexprlem4  11034  pceu  16779  4sqlem12  16889  vdwapun  16907  gsumval3eu  19772  dprd2d2  19914  znleval  21110  metrest  24033  sleadd1  27472  addsuniflem  27484  addsasslem1  27486  addsasslem2  27487  mulsuniflem  27604  addsdilem1  27606  addsdilem2  27607  mulsasslem1  27618  mulsasslem2  27619  fmptcof2  31882  fpwrelmapffslem  31957  cusgredgex  34112  dfdm5  34744  dfrn5  34745  elima4  34747  brtxp  34852  brpprod  34857  elfix  34875  dfiota3  34895  brimg  34909  brapply  34910  brsuccf  34913  funpartlem  34914  brrestrict  34921  dfrecs2  34922  dfrdg4  34923  lshpsmreu  37979  isopos  38050  islpln5  38406  islvol5  38450  cdlemftr3  39436  dibelval3  40018  dicelval3  40051  mapdpglem3  40546  hdmapglem7a  40798  diophrex  41513