Theorem ceqsexv 3504

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1560   = wceq 1562  ∃wex 1801   ∈ wcel 2144  Vcvv 3456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-clel 2839

This theorem is referenced by:  ceqsex2v  3507  ceqsex3v  3508  gencbvex  3512  euxfr2w  3685  euxfr2  3687  inuni  5308  eqvinop  5457  elvvv  5725  dmfco  6965  fndmdif  7025  fndmin  7028  fmptco  7113  abrexco  7230  imaeqsexvOLD  7349  imaeqexov  7636  uniuni  7747  elxp4  7905  elxp5  7906  brtpos2  8214  xpsnen  9035  xpcomco  9041  xpassen  9045  brttrcl2  9671  dfac5lem2  10082  cf0  10209  ltexprlem4  10999  pceu  16884  4sqlem12  16994  vdwapun  17012  gsumval3eu  19946  dprd2d2  20088  znleval  21608  metrest  24586  leadds1  28084  addsuniflem  28096  addsasslem1  28098  addsasslem2  28099  mulsuniflem  28244  addsdilem1  28246  addsdilem2  28247  mulsasslem1  28258  mulsasslem2  28259  elreno2  28590  renegscl  28593  readdscl  28594  remulscl  28597  fmptcof2  32861  fpwrelmapffslem  32936  cusgredgex  35477  dfdm5  36128  dfrn5  36129  elima4  36131  brtxp  36233  brpprod  36238  elfix  36256  dfiota3  36276  brimg  36290  brapply  36291  lemsuccf  36294  funpartlem  36297  brrestrict  36304  dfrecs2  36305  dfrdg4  36306  lshpsmreu  39738  isopos  39809  islpln5  40164  islvol5  40208  cdlemftr3  41194  dibelval3  41776  dicelval3  41809  mapdpglem3  42304  hdmapglem7a  42556  diophrex  43361