Theorem ceqsexv 3495

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803

This theorem is referenced by:  ceqsexv2dOLD  3497  ceqsex2v  3499  ceqsex3v  3500  gencbvex  3504  euxfr2w  3688  euxfr2  3690  inuni  5300  eqvinop  5442  elvvv  5707  dmfco  6940  fndmdif  6997  fndmin  7000  fmptco  7084  abrexco  7201  imaeqsexvOLD  7321  imaeqexov  7608  uniuni  7719  elxp4  7879  elxp5  7880  brtpos2  8189  xpsnen  9003  xpcomco  9009  xpassen  9013  brttrcl2  9646  dfac5lem2  10056  cf0  10183  ltexprlem4  10971  pceu  16795  4sqlem12  16905  vdwapun  16923  gsumval3eu  19820  dprd2d2  19962  znleval  21498  metrest  24447  sleadd1  27938  addsuniflem  27950  addsasslem1  27952  addsasslem2  27953  mulsuniflem  28094  addsdilem1  28096  addsdilem2  28097  mulsasslem1  28108  mulsasslem2  28109  renegscl  28404  readdscl  28405  remulscl  28408  fmptcof2  32633  fpwrelmapffslem  32707  cusgredgex  35104  dfdm5  35755  dfrn5  35756  elima4  35758  brtxp  35863  brpprod  35868  elfix  35886  dfiota3  35906  brimg  35920  brapply  35921  brsuccf  35924  funpartlem  35925  brrestrict  35932  dfrecs2  35933  dfrdg4  35934  lshpsmreu  39097  isopos  39168  islpln5  39524  islvol5  39568  cdlemftr3  40554  dibelval3  41136  dicelval3  41169  mapdpglem3  41664  hdmapglem7a  41916  diophrex  42758