Theorem csbeq1a 3136

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 3135	. 2 |- [_ x / x ]_ B = B
2		csbeq1 3130	. 2 |- ( x = A -> [_ x / x ]_ B = [_ A / x ]_ B )
3	1, 2	eqtr3id 2278	1 |- ( x = A -> B = [_ A / x ]_ B )

Syntax hints:   -> wi 4   = wceq 1397   [_csb 3127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-sbc 3032  df-csb 3128

This theorem is referenced by:  csbhypf  3166  csbiebt  3167  sbcnestgf  3179  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rspc2vd  3196  csbing  3414  disjnims  4079  invdisjrab  4082  disjiun  4083  sbcbrg  4143  moop2  4344  pofun  4409  eusvnf  4550  opeliunxp  4781  elrnmpt1  4983  resmptf  5063  csbima12g  5097  fvmpts  5724  fvmpt2  5730  mptfvex  5732  fmptco  5813  fmptcof  5814  fmptcos  5815  elabrex  5898  elabrexg  5899  fliftfuns  5939  riotaeqimp  5996  csbov123g  6057  ovmpos  6145  fvmpopr2d  6158  csbopeq1a  6351  mpomptsx  6362  dmmpossx  6364  fmpox  6365  mpofvex  6370  fmpoco  6381  disjxp1  6401  eqerlem  6733  qliftfuns  6788  mptelixpg  6903  xpf1o  7030  iunfidisj  7145  cc3  7487  seq3f1olemstep  10777  seq3f1olemp  10778  sumeq2  11921  sumfct  11936  sumrbdclem  11940  summodclem3  11943  summodclem2a  11944  zsumdc  11947  fsumgcl  11949  fsum3  11950  isumss  11954  isumss2  11956  fsum3cvg2  11957  fsumzcl2  11968  fsumsplitf  11971  sumsnf  11972  sumsns  11978  fsumsplitsnun  11982  fsum2dlemstep  11997  fsumcnv  12000  fisumcom2  12001  fsumshftm  12008  fisum0diag2  12010  fsummulc2  12011  fsum00  12025  fsumabs  12028  fsumrelem  12034  fsumiun  12040  isumshft  12053  mertenslem2  12099  prodeq2  12120  prodrbdclem  12134  prodmodclem3  12138  prodmodclem2a  12139  zproddc  12142  fprodseq  12146  fprodntrivap  12147  prodfct  12150  prodssdc  12152  fprodmul  12154  prodsnf  12155  fprodm1s  12164  fprodp1s  12165  prodsns  12166  fprodcl2lem  12168  fprodcllemf  12176  fprodabs  12179  fprodap0  12184  fprod2dlemstep  12185  fprodcnv  12188  fprodcom2fi  12189  fprodrec  12192  fproddivapf  12194  fprodsplitf  12195  fprodsplit1f  12197  fprodap0f  12199  fprodle  12203  fprodmodd  12204  pcmpt  12918  pcmptdvds  12920  ctiunctlemudc  13060  ctiunctlemf  13061  ctiunctal  13064  gsumfzfsumlemm  14604  iuncld  14842  fsumcncntop  15294  limcmpted  15390  dvmptfsum  15452  fsumdvdsmul  15718