Theorem ceqsexv 3485

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2110  Vcvv 3434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2804

This theorem is referenced by:  ceqsexv2dOLD  3487  ceqsex2v  3489  ceqsex3v  3490  gencbvex  3494  euxfr2w  3677  euxfr2  3679  inuni  5286  eqvinop  5425  elvvv  5690  dmfco  6913  fndmdif  6970  fndmin  6973  fmptco  7057  abrexco  7173  imaeqsexvOLD  7292  imaeqexov  7579  uniuni  7690  elxp4  7847  elxp5  7848  brtpos2  8157  xpsnen  8969  xpcomco  8975  xpassen  8979  brttrcl2  9599  dfac5lem2  10007  cf0  10134  ltexprlem4  10922  pceu  16750  4sqlem12  16860  vdwapun  16878  gsumval3eu  19809  dprd2d2  19951  znleval  21484  metrest  24432  sleadd1  27925  addsuniflem  27937  addsasslem1  27939  addsasslem2  27940  mulsuniflem  28081  addsdilem1  28083  addsdilem2  28084  mulsasslem1  28095  mulsasslem2  28096  renegscl  28393  readdscl  28394  remulscl  28397  fmptcof2  32629  fpwrelmapffslem  32705  cusgredgex  35134  dfdm5  35785  dfrn5  35786  elima4  35788  brtxp  35893  brpprod  35898  elfix  35916  dfiota3  35936  brimg  35950  brapply  35951  brsuccf  35954  funpartlem  35955  brrestrict  35962  dfrecs2  35963  dfrdg4  35964  lshpsmreu  39127  isopos  39198  islpln5  39553  islvol5  39597  cdlemftr3  40583  dibelval3  41165  dicelval3  41198  mapdpglem3  41693  hdmapglem7a  41945  diophrex  42787