Theorem csbied 3360

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

Step	Hyp	Ref	Expression
1		nfv 1755	. 2 |- F/ x ph
2		nfcvd 2565	. 2 |- ( ph -> F/_ x C )
3		csbied.1	. 2 |- ( ph -> A e. V )
4		csbied.2	. 2 |- ( ( ph /\ x = A ) -> B = C )
5	1, 2, 3, 4	csbiedf 3354	1 |- ( ph -> [_ A / x ]_ B = C )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1872   [_csb 3333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-sbc 3238  df-csb 3334

This theorem is referenced by:  csbied2  3361  fvmptd  5909  mpt2sn  6837  cantnfval  8120  fprodeq0  13967  imasval  15349  imasvalOLD  15350  gsumvalx  16451  mulgfval  16697  isga  16883  symgval  16958  gexval  17165  gexvalOLD  17167  telgsumfz  17558  telgsumfz0  17560  telgsum  17562  isirred  17865  psrval  18524  mplval  18590  opsrval  18636  evlsval  18680  evls1fval  18846  evl1fval  18854  znval  19043  scmatval  19466  pmatcollpw3lem  19744  pm2mpval  19756  pm2mpmhmlem2  19780  chfacffsupp  19817  tsmsval2  21081  dvfsumle  22910  dvfsumabs  22912  dvfsumlem1  22915  dvfsum2  22923  itgparts  22936  q1pval  23041  r1pval  23044  rlimcnp2  23829  vmaval  23977  fsumdvdscom  24051  fsumvma  24078  logexprlim  24090  dchrval  24099  dchrisumlema  24263  dchrisumlem2  24265  dchrisumlem3  24266  ttgval  24842  msrval  30123  poimirlem1  31848  poimirlem2  31849  poimirlem6  31853  poimirlem7  31854  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem23  31870  poimirlem24  31871  fsumshftd  32435  fsumshftdOLD  32436  hlhilset  35417  mendval  35962  ply1mulgsumlem3  39773  ply1mulgsumlem4  39774  ply1mulgsum  39775  dmatALTval  39786