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

Theorem csbied 3932
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 3895 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
2 csbied.1 . . . . . 6 (𝜑𝐴𝑉)
3 csbied.2 . . . . . . 7 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
43eleq2d 2820 . . . . . 6 ((𝜑𝑥 = 𝐴) → (𝑧𝐵𝑧𝐶))
52, 4sbcied 3823 . . . . 5 (𝜑 → ([𝐴 / 𝑥]𝑧𝐵𝑧𝐶))
65alrimiv 1931 . . . 4 (𝜑 → ∀𝑧([𝐴 / 𝑥]𝑧𝐵𝑧𝐶))
7 df-clab 2711 . . . . . . 7 (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝑦𝐵)
8 eleq1w 2817 . . . . . . . . 9 (𝑦 = 𝑧 → (𝑦𝐵𝑧𝐵))
98sbcbidv 3837 . . . . . . . 8 (𝑦 = 𝑧 → ([𝐴 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑧𝐵))
109sbievw 2096 . . . . . . 7 ([𝑧 / 𝑦][𝐴 / 𝑥]𝑦𝐵[𝐴 / 𝑥]𝑧𝐵)
117, 10bitr2i 276 . . . . . 6 ([𝐴 / 𝑥]𝑧𝐵𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵})
1211bibi1i 339 . . . . 5 (([𝐴 / 𝑥]𝑧𝐵𝑧𝐶) ↔ (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
1312biimpi 215 . . . 4 (([𝐴 / 𝑥]𝑧𝐵𝑧𝐶) → (𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
146, 13sylg 1826 . . 3 (𝜑 → ∀𝑧(𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
15 dfcleq 2726 . . 3 ({𝑦[𝐴 / 𝑥]𝑦𝐵} = 𝐶 ↔ ∀𝑧(𝑧 ∈ {𝑦[𝐴 / 𝑥]𝑦𝐵} ↔ 𝑧𝐶))
1614, 15sylibr 233 . 2 (𝜑 → {𝑦[𝐴 / 𝑥]𝑦𝐵} = 𝐶)
171, 16eqtrid 2785 1 (𝜑𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  [wsb 2068  wcel 2107  {cab 2710  [wsbc 3778  csb 3894
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  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779  df-csb 3895
This theorem is referenced by:  csbied2  3934  rspc2vd  3945  el2mpocl  8072  mposn  8089  cantnfval  9663  fprodeq0  15919  imasval  17457  gsumvalx  18595  efmnd  18751  mulgfval  18952  mulgfvalALT  18953  isga  19155  gexval  19446  telgsumfz  19858  telgsumfz0  19860  telgsum  19862  isirred  20233  znval  21087  psrval  21468  mplval  21548  opsrval  21601  evlsval  21649  evls1fval  21838  evl1fval  21847  scmatval  22006  pmatcollpw3lem  22285  pm2mpval  22297  pm2mpmhmlem2  22321  chfacffsupp  22358  tsmsval2  23634  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsum2  25551  itgparts  25564  q1pval  25671  r1pval  25674  rlimcnp2  26471  vmaval  26617  fsumdvdscom  26689  fsumvma  26716  logexprlim  26728  dchrval  26737  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  mulsval  27565  ttgval  28126  ttgvalOLD  28127  finsumvtxdg2sstep  28806  idlsrgval  32617  rprmval  32633  gsummoncoe1fzo  32668  msrval  34529  gg-dvfsumle  35182  poimirlem1  36489  poimirlem2  36490  poimirlem6  36494  poimirlem7  36495  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem23  36511  poimirlem24  36512  fsumshftd  37822  hlhilset  40805  prjspval  41345  mendval  41925  ply1mulgsumlem3  47069  ply1mulgsumlem4  47070  ply1mulgsum  47071  dmatALTval  47081
  Copyright terms: Public domain W3C validator