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

Theorem csbied 3461
 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.)
Hypotheses
Ref Expression
csbied.1
csbied.2
Assertion
Ref Expression
csbied
Distinct variable groups:   ,   ,   ,

Proof of Theorem csbied
StepHypRef Expression
1 nfv 1707 . 2
2 nfcvd 2620 . 2
3 csbied.1 . 2
4 csbied.2 . 2
51, 2, 3, 4csbiedf 3455 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  [_csb 3434 This theorem is referenced by:  csbied2  3462  fvmptd  5961  mpt2sn  6891  cantnfval  8108  cantnfvalOLD  8138  fprodeq0  13779  imasval  14908  gsumvalx  15897  mulgfval  16143  isga  16329  symgval  16404  gexval  16598  telgsumfz  17019  telgsumfz0  17021  telgsum  17023  isirred  17348  psrval  18011  mplval  18084  opsrval  18139  evlsval  18188  evls1fval  18356  evl1fval  18364  znval  18572  scmatval  19006  pmatcollpw3lem  19284  pm2mpval  19296  pm2mpmhmlem2  19320  chfacffsupp  19357  tsmsval2  20628  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  dvfsum2  22435  itgparts  22448  q1pval  22554  r1pval  22557  rlimcnp2  23296  vmaval  23387  fsumdvdscom  23461  fsumvma  23488  logexprlim  23500  dchrval  23509  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  ttgval  24178  msrval  28898  mendval  31132  ply1mulgsumlem3  32988  ply1mulgsumlem4  32989  ply1mulgsum  32990  dmatALTval  33001  fsumshftd  34682  fsumshftdOLD  34683  hlhilset  37664 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sbc 3328  df-csb 3435
 Copyright terms: Public domain W3C validator