Theorem ceqsexv 3498

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2212. (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 1875	. . 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 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835

This theorem is used by:  ceqsex2v  3501  ceqsex3v  3502  gencbvex  3506  euxfr2w  3677  euxfr2  3679  inuni  5310  eqvinop  5455  eqvinot  5456  elvvv  5726  dmfco  6981  fndmdif  7041  fndmin  7044  fmptco  7130  abrexco  7248  imaeqexov  7659  uniuni  7776  elxp4  7934  elxp5  7935  brtpos2  8249  xpsnen  9080  xpcomco  9086  xpassen  9090  brttrcl2  9715  dfac5lem2  10203  cf0  10328  ltexprlem4  11124  pceu  17024  4sqlem12  17134  vdwapun  17152  gsumval3eu  20118  dprd2d2  20260  znleval  21860  metrest  24843  leadds1  28375  addsuniflem  28387  addsasslem1  28389  addsasslem2  28390  mulsuniflem  28535  addsdilem1  28537  addsdilem2  28538  mulsasslem1  28549  mulsasslem2  28550  elreno2  28881  renegscl  28884  readdscl  28885  remulscl  28888  fmptcof2  33251  fpwrelmapffslem  33324  cusgredgex  35906  dfdm5  36537  dfrn5  36538  elima4  36540  brtxp  36642  brpprod  36647  elfix  36665  dfiota3  36685  brimg  36699  brapply  36700  lemsuccf  36703  funpartlem  36706  brrestrict  36713  dfrecs2  36714  dfrdg4  36715  lshpsmreu  40167  isopos  40238  islpln5  40593  islvol5  40637  cdlemftr3  41623  dibelval3  42205  dicelval3  42238  mapdpglem3  42733  hdmapglem7a  42985  diophrex  43786