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

Theorem ceqsexv 3447
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2179. (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 480 . . 3 ((𝑥 = 𝐴𝜑) → 𝜓)
32exlimiv 1937 . 2 (∃𝑥(𝑥 = 𝐴𝜑) → 𝜓)
41biimprcd 253 . . . 4 (𝜓 → (𝑥 = 𝐴𝜑))
54alrimiv 1934 . . 3 (𝜓 → ∀𝑥(𝑥 = 𝐴𝜑))
6 ceqsexv.1 . . . 4 𝐴 ∈ V
76isseti 3415 . . 3 𝑥 𝑥 = 𝐴
8 exintr 1899 . . 3 (∀𝑥(𝑥 = 𝐴𝜑) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥(𝑥 = 𝐴𝜑)))
95, 7, 8mpisyl 21 . 2 (𝜓 → ∃𝑥(𝑥 = 𝐴𝜑))
103, 9impbii 212 1 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1540   = wceq 1542  wex 1786  wcel 2114  Vcvv 3400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-clel 2812
This theorem is referenced by:  ceqsexv2d  3449  ceqsex2v  3451  ceqsex3v  3452  gencbvex  3456  euxfr2w  3624  euxfr2  3626  inuni  5221  eqvinop  5354  elvvv  5608  dmfco  6776  fndmdif  6831  fndmin  6834  fmptco  6913  abrexco  7026  uniuni  7515  elxp4  7665  elxp5  7666  brtpos2  7939  xpsnen  8662  xpcomco  8668  xpassen  8672  dfac5lem2  9636  cf0  9763  ltexprlem4  10551  pceu  16295  4sqlem12  16404  vdwapun  16422  gsumval3eu  19155  dprd2d2  19297  znleval  20385  metrest  23289  fmptcof2  30581  fpwrelmapffslem  30654  cusgredgex  32666  imaeqsexv  33276  dfdm5  33333  dfrn5  33334  elima4  33336  brtxp  33837  brpprod  33842  elfix  33860  dfiota3  33880  brimg  33894  brapply  33895  brsuccf  33898  funpartlem  33899  brrestrict  33906  dfrecs2  33907  dfrdg4  33908  lshpsmreu  36778  isopos  36849  islpln5  37204  islvol5  37248  cdlemftr3  38234  dibelval3  38816  dicelval3  38849  mapdpglem3  39344  hdmapglem7a  39596  diophrex  40209
  Copyright terms: Public domain W3C validator