MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ceqsexv Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 ceqsexv.2 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
21biimpa 477 . . 3 ((𝑥 = 𝐴𝜑) → 𝜓)
32exlimiv 1934 . 2 (∃𝑥(𝑥 = 𝐴𝜑) → 𝜓)
41biimprcd 249 . . . 4 (𝜓 → (𝑥 = 𝐴𝜑))
54alrimiv 1931 . . 3 (𝜓 → ∀𝑥(𝑥 = 𝐴𝜑))
6 ceqsexv.1 . . . 4 𝐴 ∈ V
76isseti 3448 . . 3 𝑥 𝑥 = 𝐴
8 exintr 1896 . . 3 (∀𝑥(𝑥 = 𝐴𝜑) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥(𝑥 = 𝐴𝜑)))
95, 7, 8mpisyl 21 . 2 (𝜓 → ∃𝑥(𝑥 = 𝐴𝜑))
103, 9impbii 208 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator