Theorem ceqsexv 3479

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 3470	. . 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 3430

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  3481  ceqsex2v  3483  ceqsex3v  3484  gencbvex  3488  euxfr2w  3667  euxfr2  3669  inuni  5292  eqvinop  5441  elvvv  5707  dmfco  6937  fndmdif  6995  fndmin  6998  fmptco  7083  abrexco  7199  imaeqsexvOLD  7318  imaeqexov  7605  uniuni  7716  elxp4  7873  elxp5  7874  brtpos2  8182  xpsnen  8999  xpcomco  9005  xpassen  9009  brttrcl2  9635  dfac5lem2  10046  cf0  10173  ltexprlem4  10962  pceu  16817  4sqlem12  16927  vdwapun  16945  gsumval3eu  19879  dprd2d2  20021  znleval  21534  metrest  24489  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  mulsuniflem  28141  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  elreno2  28487  renegscl  28490  readdscl  28491  remulscl  28494  fmptcof2  32730  fpwrelmapffslem  32805  cusgredgex  35304  dfdm5  35955  dfrn5  35956  elima4  35958  brtxp  36060  brpprod  36065  elfix  36083  dfiota3  36103  brimg  36117  brapply  36118  lemsuccf  36121  funpartlem  36124  brrestrict  36131  dfrecs2  36132  dfrdg4  36133  lshpsmreu  39555  isopos  39626  islpln5  39981  islvol5  40025  cdlemftr3  41011  dibelval3  41593  dicelval3  41626  mapdpglem3  42121  hdmapglem7a  42373  diophrex  43207