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

Theorem csbied 3376
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 1769 . 2  |-  F/ x ph
2 nfcvd 2613 . 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 3370 1  |-  ( ph  ->  [_ A  /  x ]_ B  =  C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452    e. wcel 1904   [_csb 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-sbc 3256  df-csb 3350
This theorem is referenced by:  csbied2  3377  fvmptd  5969  mpt2sn  6906  cantnfval  8191  fprodeq0  14106  imasval  15489  imasvalOLD  15490  gsumvalx  16591  mulgfval  16837  isga  17023  symgval  17098  gexval  17305  gexvalOLD  17307  telgsumfz  17698  telgsumfz0  17700  telgsum  17702  isirred  18005  psrval  18663  mplval  18729  opsrval  18775  evlsval  18819  evls1fval  18985  evl1fval  18993  znval  19183  scmatval  19606  pmatcollpw3lem  19884  pm2mpval  19896  pm2mpmhmlem2  19920  chfacffsupp  19957  tsmsval2  21222  dvfsumle  23052  dvfsumabs  23054  dvfsumlem1  23057  dvfsum2  23065  itgparts  23078  q1pval  23183  r1pval  23186  rlimcnp2  23971  vmaval  24119  fsumdvdscom  24193  fsumvma  24220  logexprlim  24232  dchrval  24241  dchrisumlema  24405  dchrisumlem2  24407  dchrisumlem3  24408  ttgval  24984  msrval  30248  poimirlem1  32005  poimirlem2  32006  poimirlem6  32010  poimirlem7  32011  poimirlem10  32014  poimirlem11  32015  poimirlem12  32016  poimirlem23  32027  poimirlem24  32028  fsumshftd  32587  fsumshftdOLD  32588  hlhilset  35576  mendval  36120  ply1mulgsumlem3  40688  ply1mulgsumlem4  40689  ply1mulgsum  40690  dmatALTval  40701
  Copyright terms: Public domain W3C validator