Theorem ceqsexv 3509

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844

This theorem is referenced by:  ceqsex2v  3512  ceqsex3v  3513  gencbvex  3517  euxfr2w  3690  euxfr2  3692  inuni  5321  eqvinop  5470  elvvv  5738  dmfco  6978  fndmdif  7038  fndmin  7041  fmptco  7126  abrexco  7243  imaeqsexvOLD  7362  imaeqexov  7649  uniuni  7761  elxp4  7919  elxp5  7920  brtpos2  8228  xpsnen  9049  xpcomco  9055  xpassen  9059  brttrcl2  9683  dfac5lem2  10108  cf0  10234  ltexprlem4  11024  pceu  16906  4sqlem12  17016  vdwapun  17034  gsumval3eu  19974  dprd2d2  20116  znleval  21673  metrest  24650  leadds1  28148  addsuniflem  28160  addsasslem1  28162  addsasslem2  28163  mulsuniflem  28308  addsdilem1  28310  addsdilem2  28311  mulsasslem1  28322  mulsasslem2  28323  elreno2  28654  renegscl  28657  readdscl  28658  remulscl  28661  fmptcof2  32943  fpwrelmapffslem  33018  cusgredgex  35547  dfdm5  36198  dfrn5  36199  elima4  36201  brtxp  36303  brpprod  36308  elfix  36326  dfiota3  36346  brimg  36360  brapply  36361  lemsuccf  36364  funpartlem  36367  brrestrict  36374  dfrecs2  36375  dfrdg4  36376  lshpsmreu  39808  isopos  39879  islpln5  40234  islvol5  40278  cdlemftr3  41264  dibelval3  41846  dicelval3  41879  mapdpglem3  42374  hdmapglem7a  42626  diophrex  43433