Theorem csbied 3414

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   [_csb 3388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-sbc 3287  df-csb 3389

This theorem is referenced by:  csbied2  3415  fvmptd  5880  cantnfval  7979  cantnfvalOLD  8009  imasval  14553  gsumvalx  15606  mulgfval  15732  isga  15913  symgval  15988  gexval  16183  isirred  16899  psrval  17537  mplval  17610  opsrval  17665  evlsval  17714  evls1fval  17865  evl1fval  17873  znval  18077  tsmsval2  19818  dvfsumle  21611  dvfsumabs  21613  dvfsumlem1  21616  dvfsum2  21624  itgparts  21637  q1pval  21743  r1pval  21746  rlimcnp2  22478  vmaval  22569  fsumdvdscom  22643  fsumvma  22670  logexprlim  22682  dchrval  22691  dchrisumlema  22855  dchrisumlem2  22857  dchrisumlem3  22858  ttgval  23258  fprodeq0  27622  mendval  29680  mpt2sn  30863  telescfzgsumis  30954  telescfzgsum0is  30956  ply1mulgsumlem3  30990  ply1mulgsumlem4  30991  ply1mulgsum  30992  pmatcollpwfsupp  31231  pmatcollpw4  31242  pmatcollpw4fi  31243  pmattomply1mhmlem0  31274  pmattomply1mhmlem1  31275  pmattomply1mhmlem2  31276  chfacffsupp  31312  fsumshftd  32910  fsumshftdOLD  32911  hlhilset  35890