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

Step	Hyp	Ref	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 )
5	1, 2, 3, 4	csbiedf 3370	1 |- ( ph -> [_ A / x ]_ B = C )

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