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

Theorem csbied 3285
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  |-  ( ph  ->  A  e.  V )
csbied.2  |-  ( (
ph  /\  x  =  A )  ->  B  =  C )
Assertion
Ref Expression
csbied  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
Distinct variable groups:    x, A    x, C    ph, x
Allowed substitution hints:    B( x)    V( x)

Proof of Theorem csbied
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 nfcvd 2572 . 2  |-  ( ph  -> 
F/_ x C )
3 csbied.1 . 2  |-  ( ph  ->  A  e.  V )
4 csbied.2 . 2  |-  ( (
ph  /\  x  =  A )  ->  B  =  C )
51, 2, 3, 4csbiedf 3280 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   [_csb 3243
This theorem is referenced by:  csbied2  3286  fvmptd  5802  cantnfval  7615  imasval  13729  gsumvalx  14766  mulgfval  14883  isga  15060  symgval  15086  gexval  15204  isirred  15796  psrval  16421  mplval  16484  opsrval  16527  znval  16808  tsmsval2  18151  dvfsumle  19897  dvfsumabs  19899  dvfsumlem1  19902  dvfsum2  19910  itgparts  19923  evlsval  19932  evl1fval  19939  q1pval  20068  r1pval  20071  rlimcnp2  20797  vmaval  20888  fsumdvdscom  20962  fsumvma  20989  logexprlim  21001  dchrval  21010  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  fprodeq0  25291  mendval  27459  hlhilset  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sbc 3154  df-csb 3244
  Copyright terms: Public domain W3C validator