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

Theorem csbied 3930
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) Reduce axiom usage. (Revised by Gino Giotto, 15-Oct-2024.)
Hypotheses
Ref Expression
csbied.1 (𝜑𝐴𝑉)
csbied.2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
Assertion
Ref Expression
csbied (𝜑𝐴 / 𝑥𝐵 = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem csbied
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-csb 3893 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
2 csbied.1 . . . . . 6 (𝜑𝐴𝑉)
3 csbied.2 . . . . . . 7 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
43eleq2d 2815 . . . . . 6 ((𝜑𝑥 = 𝐴) → (𝑧𝐵𝑧𝐶))
52, 4sbcied 3822 . . . . 5 (𝜑 → ([𝐴 / 𝑥]𝑧𝐵𝑧𝐶))
65alrimiv 1923 . . . 4 (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧𝐵𝑧𝐶))
7 df-clab 2706 . . . . . . 7 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦𝐵)
8 eleq1w 2812 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑦𝐵𝑧𝐵))
98sbcbidv 3836 . . . . . . . 8 (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑧𝐵))
109sbievw 2088 . . . . . . 7 ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑧𝐵)
117, 10bitr2i 276 . . . . . 6 ([𝐴 / 𝑥]𝑧𝐵𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵})
1211bibi1i 338 . . . . 5 (([𝐴 / 𝑥]𝑧𝐵𝑧𝐶) ↔ (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
1312biimpi 215 . . . 4 (([𝐴 / 𝑥]𝑧𝐵𝑧𝐶) → (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
146, 13sylg 1818 . . 3 (𝜑 → ∀𝑧(𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
15 dfcleq 2721 . . 3 ({𝑦[𝐴 / 𝑥]𝑦𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
1614, 15sylibr 233 . 2 (𝜑 → {𝑦[𝐴 / 𝑥]𝑦𝐵} = 𝐶)
171, 16eqtrid 2780 1 (𝜑𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wal 1532   = wceq 1534  [wsb 2060  wcel 2099  {cab 2705  [wsbc 3776  csb 3892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-sbc 3777  df-csb 3893
This theorem is referenced by:  csbied2  3932  rspc2vd  3943  el2mpocl  8091  mposn  8108  cantnfval  9692  fprodeq0  15952  imasval  17493  gsumvalx  18636  efmnd  18822  mulgfval  19025  mulgfvalALT  19026  isga  19242  gexval  19533  telgsumfz  19945  telgsumfz0  19947  telgsum  19949  isirred  20358  znval  21465  psrval  21848  mplval  21931  opsrval  21984  evlsval  22032  evls1fval  22238  evl1fval  22247  scmatval  22419  pmatcollpw3lem  22698  pm2mpval  22710  pm2mpmhmlem2  22734  chfacffsupp  22771  tsmsval2  24047  dvfsumle  25967  dvfsumleOLD  25968  dvfsumabs  25970  dvfsumlem1  25973  dvfsum2  25982  itgparts  25995  q1pval  26103  r1pval  26106  rlimcnp2  26911  vmaval  27058  fsumdvdscom  27130  fsumvma  27159  logexprlim  27171  dchrval  27180  dchrisumlema  27434  dchrisumlem2  27436  dchrisumlem3  27437  mulsval  28022  ttgval  28692  ttgvalOLD  28693  finsumvtxdg2sstep  29376  idlsrgval  33227  rprmval  33243  gsummoncoe1fzo  33268  msrval  35148  poimirlem1  37094  poimirlem2  37095  poimirlem6  37099  poimirlem7  37100  poimirlem10  37103  poimirlem11  37104  poimirlem12  37105  poimirlem23  37116  poimirlem24  37117  fsumshftd  38424  hlhilset  41407  isprimroot  41564  prjspval  42027  mendval  42607  ply1mulgsumlem3  47456  ply1mulgsumlem4  47457  ply1mulgsum  47458  dmatALTval  47468
  Copyright terms: Public domain W3C validator