Theorem ceqsexv 3501

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3453

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2837

This theorem is used by:  ceqsex2v  3504  ceqsex3v  3505  gencbvex  3509  euxfr2w  3681  euxfr2  3683  inuni  5318  eqvinop  5467  elvvv  5735  dmfco  6978  fndmdif  7038  fndmin  7041  fmptco  7126  abrexco  7244  imaeqexov  7655  uniuni  7764  elxp4  7922  elxp5  7923  brtpos2  8233  xpsnen  9062  xpcomco  9068  xpassen  9072  brttrcl2  9696  dfac5lem2  10130  cf0  10255  ltexprlem4  11051  pceu  16942  4sqlem12  17052  vdwapun  17070  gsumval3eu  20032  dprd2d2  20174  znleval  21768  metrest  24751  leadds1  28252  addsuniflem  28264  addsasslem1  28266  addsasslem2  28267  mulsuniflem  28412  addsdilem1  28414  addsdilem2  28415  mulsasslem1  28426  mulsasslem2  28427  elreno2  28758  renegscl  28761  readdscl  28762  remulscl  28765  fmptcof2  33117  fpwrelmapffslem  33190  cusgredgex  35707  dfdm5  36339  dfrn5  36340  elima4  36342  brtxp  36444  brpprod  36449  elfix  36467  dfiota3  36487  brimg  36501  brapply  36502  lemsuccf  36505  funpartlem  36508  brrestrict  36515  dfrecs2  36516  dfrdg4  36517  lshpsmreu  39969  isopos  40040  islpln5  40395  islvol5  40439  cdlemftr3  41425  dibelval3  42007  dicelval3  42040  mapdpglem3  42535  hdmapglem7a  42787  diophrex  43607