Theorem ceqsexv 3498

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2213. (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 3489	. . 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 3450

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 2835

This theorem is used by:  ceqsex2v  3501  ceqsex3v  3502  gencbvex  3506  euxfr2w  3677  euxfr2  3679  inuni  5310  eqvinop  5455  elvvv  5723  dmfco  6969  fndmdif  7029  fndmin  7032  fmptco  7118  abrexco  7236  imaeqexov  7647  uniuni  7759  elxp4  7917  elxp5  7918  brtpos2  8227  xpsnen  9058  xpcomco  9064  xpassen  9068  brttrcl2  9693  dfac5lem2  10174  cf0  10299  ltexprlem4  11095  pceu  16985  4sqlem12  17095  vdwapun  17113  gsumval3eu  20079  dprd2d2  20221  znleval  21821  metrest  24804  leadds1  28308  addsuniflem  28320  addsasslem1  28322  addsasslem2  28323  mulsuniflem  28468  addsdilem1  28470  addsdilem2  28471  mulsasslem1  28482  mulsasslem2  28483  elreno2  28814  renegscl  28817  readdscl  28818  remulscl  28821  fmptcof2  33184  fpwrelmapffslem  33257  cusgredgex  35827  dfdm5  36459  dfrn5  36460  elima4  36462  brtxp  36564  brpprod  36569  elfix  36587  dfiota3  36607  brimg  36621  brapply  36622  lemsuccf  36625  funpartlem  36628  brrestrict  36635  dfrecs2  36636  dfrdg4  36637  lshpsmreu  40086  isopos  40157  islpln5  40512  islvol5  40556  cdlemftr3  41542  dibelval3  42124  dicelval3  42157  mapdpglem3  42652  hdmapglem7a  42904  diophrex  43724