Theorem csbied 3447

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 1712	. 2 |- F/ x ph
2		nfcvd 2617	. 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 3441	1 |- ( ph -> [_ A / x ]_ B = C )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   e. wcel 1823   [_csb 3420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-sbc 3325  df-csb 3421

This theorem is referenced by:  csbied2  3448  fvmptd  5936  mpt2sn  6864  cantnfval  8078  cantnfvalOLD  8108  fprodeq0  13861  imasval  15000  gsumvalx  16096  mulgfval  16342  isga  16528  symgval  16603  gexval  16797  telgsumfz  17214  telgsumfz0  17216  telgsum  17218  isirred  17543  psrval  18206  mplval  18279  opsrval  18334  evlsval  18383  evls1fval  18551  evl1fval  18559  znval  18747  scmatval  19173  pmatcollpw3lem  19451  pm2mpval  19463  pm2mpmhmlem2  19487  chfacffsupp  19524  tsmsval2  20794  dvfsumle  22588  dvfsumabs  22590  dvfsumlem1  22593  dvfsum2  22601  itgparts  22614  q1pval  22720  r1pval  22723  rlimcnp2  23494  vmaval  23585  fsumdvdscom  23659  fsumvma  23686  logexprlim  23698  dchrval  23707  dchrisumlema  23871  dchrisumlem2  23873  dchrisumlem3  23874  ttgval  24380  msrval  29162  mendval  31373  ply1mulgsumlem3  33242  ply1mulgsumlem4  33243  ply1mulgsum  33244  dmatALTval  33255  fsumshftd  35079  fsumshftdOLD  35080  hlhilset  38061