Theorem ceqsexv 3502

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2216. (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 3493	. . 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 2147  Vcvv 3454

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  ceqsex2v  3505  ceqsex3v  3506  gencbvex  3510  euxfr2w  3681  euxfr2  3683  inuni  5315  eqvinop  5460  eqvinot  5461  elvvv  5732  dmfco  7001  fndmdif  7061  fndmin  7064  fmptco  7151  abrexco  7268  imaeqexov  7680  uniuni  7797  elxp4  7955  elxp5  7956  brtpos2  8274  xpsnen  9105  xpcomco  9111  xpassen  9115  brttrcl2  9739  dfac5lem2  10227  cf0  10352  ltexprlem4  11148  pceu  17050  4sqlem12  17160  vdwapun  17178  gsumval3eu  20145  dprd2d2  20287  znleval  21887  metrest  24870  leadds1  28402  addsuniflem  28414  addsasslem1  28416  addsasslem2  28417  mulsuniflem  28562  addsdilem1  28564  addsdilem2  28565  mulsasslem1  28576  mulsasslem2  28577  elreno2  28908  renegscl  28911  readdscl  28912  remulscl  28915  fmptcof2  33320  fpwrelmapffslem  33391  cusgredgex  36062  dfdm5  36714  dfrn5  36715  elima4  36717  brtxp  36819  brpprod  36824  elfix  36842  dfiota3  36862  brimg  36876  brapply  36877  lemsuccf  36880  funpartlem  36883  brrestrict  36890  dfrecs2  36891  dfrdg4  36892  lshpsmreu  40357  isopos  40428  islpln5  40783  islvol5  40827  cdlemftr3  41813  dibelval3  42395  dicelval3  42428  mapdpglem3  42923  hdmapglem7a  43175  diophrex  43977