Theorem ceqsexv 3502

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 1872	. . 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 400  ∀wal 1567   = wceq 1569  ∃wex 1808   ∈ wcel 2142  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-clel 2837

This theorem is used by:  ceqsex2v  3505  ceqsex3v  3506  gencbvex  3510  euxfr2w  3682  euxfr2  3684  inuni  5319  eqvinop  5468  elvvv  5736  dmfco  6977  fndmdif  7037  fndmin  7040  fmptco  7125  abrexco  7242  imaeqsexvOLD  7363  imaeqexov  7650  uniuni  7759  elxp4  7917  elxp5  7918  brtpos2  8226  xpsnen  9047  xpcomco  9053  xpassen  9057  brttrcl2  9681  dfac5lem2  10115  cf0  10240  ltexprlem4  11030  pceu  16912  4sqlem12  17022  vdwapun  17040  gsumval3eu  19980  dprd2d2  20122  znleval  21715  metrest  24692  leadds1  28193  addsuniflem  28205  addsasslem1  28207  addsasslem2  28208  mulsuniflem  28353  addsdilem1  28355  addsdilem2  28356  mulsasslem1  28367  mulsasslem2  28368  elreno2  28699  renegscl  28702  readdscl  28703  remulscl  28706  fmptcof2  33013  fpwrelmapffslem  33088  cusgredgex  35622  dfdm5  36273  dfrn5  36274  elima4  36276  brtxp  36378  brpprod  36383  elfix  36401  dfiota3  36421  brimg  36435  brapply  36436  lemsuccf  36439  funpartlem  36442  brrestrict  36449  dfrecs2  36450  dfrdg4  36451  lshpsmreu  39911  isopos  39982  islpln5  40337  islvol5  40381  cdlemftr3  41367  dibelval3  41949  dicelval3  41982  mapdpglem3  42477  hdmapglem7a  42729  diophrex  43534