Theorem csbeq1a 3040

Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1a	|- ( x = A -> B = [_ A / x ]_ B )

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbid 3039	. 2 |- [_ x / x ]_ B = B
2		csbeq1 3034	. 2 |- ( x = A -> [_ x / x ]_ B = [_ A / x ]_ B )
3	1, 2	syl5eqr 2204	1 |- ( x = A -> B = [_ A / x ]_ B )

Syntax hints:   -> wi 4   = wceq 1335   [_csb 3031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938  df-csb 3032

This theorem is referenced by:  csbhypf  3069  csbiebt  3070  sbcnestgf  3082  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  csbing  3314  disjnims  3957  disjiun  3960  sbcbrg  4018  moop2  4211  pofun  4272  eusvnf  4412  opeliunxp  4640  elrnmpt1  4836  resmptf  4915  csbima12g  4946  fvmpts  5545  fvmpt2  5550  mptfvex  5552  fmptco  5632  fmptcof  5633  fmptcos  5634  elabrex  5705  fliftfuns  5745  csbov123g  5856  ovmpos  5941  csbopeq1a  6133  mpomptsx  6142  dmmpossx  6144  fmpox  6145  mpofvex  6148  fmpoco  6160  disjxp1  6180  eqerlem  6508  qliftfuns  6561  mptelixpg  6676  xpf1o  6786  iunfidisj  6887  cc3  7182  seq3f1olemstep  10393  seq3f1olemp  10394  sumeq2  11249  sumfct  11264  sumrbdclem  11267  summodclem3  11270  summodclem2a  11271  zsumdc  11274  fsumgcl  11276  fsum3  11277  isumss  11281  isumss2  11283  fsum3cvg2  11284  fsumzcl2  11295  fsumsplitf  11298  sumsnf  11299  sumsns  11305  fsumsplitsnun  11309  fsum2dlemstep  11324  fsumcnv  11327  fisumcom2  11328  fsumshftm  11335  fisum0diag2  11337  fsummulc2  11338  fsum00  11352  fsumabs  11355  fsumrelem  11361  fsumiun  11367  isumshft  11380  mertenslem2  11426  prodeq2  11447  prodrbdclem  11461  prodmodclem3  11465  prodmodclem2a  11466  zproddc  11469  fprodseq  11473  fprodntrivap  11474  prodfct  11477  prodssdc  11479  fprodmul  11481  prodsnf  11482  fprodm1s  11491  fprodp1s  11492  prodsns  11493  fprodcl2lem  11495  fprodcllemf  11503  fprodabs  11506  fprodap0  11511  fprod2dlemstep  11512  fprodcnv  11515  fprodcom2fi  11516  fprodrec  11519  fproddivapf  11521  fprodsplitf  11522  fprodsplit1f  11524  fprodap0f  11526  fprodle  11530  fprodmodd  11531  ctiunctlemudc  12149  ctiunctlemf  12150  ctiunctal  12153  iuncld  12486  fsumcncntop  12927  limcmpted  13003