Theorem ceqsexv 3486

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806

This theorem is referenced by:  ceqsexv2dOLD  3488  ceqsex2v  3490  ceqsex3v  3491  gencbvex  3495  euxfr2w  3674  euxfr2  3676  inuni  5290  eqvinop  5430  elvvv  5695  dmfco  6924  fndmdif  6981  fndmin  6984  fmptco  7068  abrexco  7184  imaeqsexvOLD  7303  imaeqexov  7590  uniuni  7701  elxp4  7858  elxp5  7859  brtpos2  8168  xpsnen  8980  xpcomco  8986  xpassen  8990  brttrcl2  9610  dfac5lem2  10021  cf0  10148  ltexprlem4  10936  pceu  16764  4sqlem12  16874  vdwapun  16892  gsumval3eu  19822  dprd2d2  19964  znleval  21497  metrest  24445  sleadd1  27938  addsuniflem  27950  addsasslem1  27952  addsasslem2  27953  mulsuniflem  28094  addsdilem1  28096  addsdilem2  28097  mulsasslem1  28108  mulsasslem2  28109  renegscl  28406  readdscl  28407  remulscl  28410  fmptcof2  32646  fpwrelmapffslem  32722  cusgredgex  35173  dfdm5  35824  dfrn5  35825  elima4  35827  brtxp  35929  brpprod  35934  elfix  35952  dfiota3  35972  brimg  35986  brapply  35987  lemsuccf  35990  funpartlem  35993  brrestrict  36000  dfrecs2  36001  dfrdg4  36002  lshpsmreu  39214  isopos  39285  islpln5  39640  islvol5  39684  cdlemftr3  40670  dibelval3  41252  dicelval3  41285  mapdpglem3  41780  hdmapglem7a  42032  diophrex  42873