Theorem ceqsexv 3480

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2172. (Revised by Gino Giotto, 12-Oct-2024.)

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		ceqsexv.2	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	biimpa 477	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝜑) → 𝜓)
3	2	exlimiv 1934	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → 𝜓)
4	1	biimprcd 249	. . . 4 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
5	4	alrimiv 1931	. . 3 ⊢ (𝜓 → ∀𝑥(𝑥 = 𝐴 → 𝜑))
6		ceqsexv.1	. . . 4 ⊢ 𝐴 ∈ V
7	6	isseti 3448	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
8		exintr 1896	. . 3 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
9	5, 7, 8	mpisyl 21	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
10	3, 9	impbii 208	1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2107  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2817

This theorem is referenced by:  ceqsexv2d  3482  ceqsex2v  3484  ceqsex3v  3485  gencbvex  3489  euxfr2w  3656  euxfr2  3658  inuni  5268  eqvinop  5402  elvvv  5663  dmfco  6873  fndmdif  6928  fndmin  6931  fmptco  7010  abrexco  7126  uniuni  7621  elxp4  7778  elxp5  7779  brtpos2  8057  xpsnen  8851  xpcomco  8858  xpassen  8862  brttrcl2  9481  dfac5lem2  9889  cf0  10016  ltexprlem4  10804  pceu  16556  4sqlem12  16666  vdwapun  16684  gsumval3eu  19514  dprd2d2  19656  znleval  20771  metrest  23689  fmptcof2  31003  fpwrelmapffslem  31076  cusgredgex  33092  imaeqsexv  33699  dfdm5  33756  dfrn5  33757  elima4  33759  brtxp  34191  brpprod  34196  elfix  34214  dfiota3  34234  brimg  34248  brapply  34249  brsuccf  34252  funpartlem  34253  brrestrict  34260  dfrecs2  34261  dfrdg4  34262  lshpsmreu  37130  isopos  37201  islpln5  37556  islvol5  37600  cdlemftr3  38586  dibelval3  39168  dicelval3  39201  mapdpglem3  39696  hdmapglem7a  39948  diophrex  40604