Theorem ceqsexv 3491

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3441

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  ceqsexv2dOLD  3493  ceqsex2v  3495  ceqsex3v  3496  gencbvex  3500  euxfr2w  3679  euxfr2  3681  inuni  5296  eqvinop  5436  elvvv  5701  dmfco  6931  fndmdif  6989  fndmin  6992  fmptco  7077  abrexco  7193  imaeqsexvOLD  7312  imaeqexov  7599  uniuni  7710  elxp4  7867  elxp5  7868  brtpos2  8177  xpsnen  8994  xpcomco  9000  xpassen  9004  brttrcl2  9628  dfac5lem2  10039  cf0  10166  ltexprlem4  10955  pceu  16779  4sqlem12  16889  vdwapun  16907  gsumval3eu  19838  dprd2d2  19980  znleval  21514  metrest  24473  leadds1  27990  addsuniflem  28002  addsasslem1  28004  addsasslem2  28005  mulsuniflem  28150  addsdilem1  28152  addsdilem2  28153  mulsasslem1  28164  mulsasslem2  28165  elreno2  28496  renegscl  28499  readdscl  28500  remulscl  28503  fmptcof2  32739  fpwrelmapffslem  32814  cusgredgex  35329  dfdm5  35980  dfrn5  35981  elima4  35983  brtxp  36085  brpprod  36090  elfix  36108  dfiota3  36128  brimg  36142  brapply  36143  lemsuccf  36146  funpartlem  36149  brrestrict  36156  dfrecs2  36157  dfrdg4  36158  lshpsmreu  39448  isopos  39519  islpln5  39874  islvol5  39918  cdlemftr3  40904  dibelval3  41486  dicelval3  41519  mapdpglem3  42014  hdmapglem7a  42266  diophrex  43095