Theorem csbeq1a 3135

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

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

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 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-sbc 3031  df-csb 3127

This theorem is referenced by:  csbhypf  3165  csbiebt  3166  sbcnestgf  3178  cbvralcsf  3189  cbvrexcsf  3190  cbvreucsf  3191  cbvrabcsf  3192  rspc2vd  3195  csbing  3413  disjnims  4080  invdisjrab  4083  disjiun  4084  sbcbrg  4144  moop2  4346  pofun  4411  eusvnf  4552  opeliunxp  4783  elrnmpt1  4985  resmptf  5065  csbima12g  5099  fvmpts  5727  fvmpt2  5733  mptfvex  5735  fmptco  5816  fmptcof  5817  fmptcos  5818  elabrex  5903  elabrexg  5904  fliftfuns  5944  riotaeqimp  6001  csbov123g  6062  ovmpos  6150  fvmpopr2d  6163  csbopeq1a  6356  mpomptsx  6367  dmmpossx  6369  fmpox  6370  mpofvex  6375  fmpoco  6386  disjxp1  6406  eqerlem  6738  qliftfuns  6793  mptelixpg  6908  xpf1o  7035  iunfidisj  7150  cc3  7492  seq3f1olemstep  10782  seq3f1olemp  10783  sumeq2  11942  sumfct  11957  sumrbdclem  11961  summodclem3  11964  summodclem2a  11965  zsumdc  11968  fsumgcl  11970  fsum3  11971  isumss  11975  isumss2  11977  fsum3cvg2  11978  fsumzcl2  11989  fsumsplitf  11992  sumsnf  11993  sumsns  11999  fsumsplitsnun  12003  fsum2dlemstep  12018  fsumcnv  12021  fisumcom2  12022  fsumshftm  12029  fisum0diag2  12031  fsummulc2  12032  fsum00  12046  fsumabs  12049  fsumrelem  12055  fsumiun  12061  isumshft  12074  mertenslem2  12120  prodeq2  12141  prodrbdclem  12155  prodmodclem3  12159  prodmodclem2a  12160  zproddc  12163  fprodseq  12167  fprodntrivap  12168  prodfct  12171  prodssdc  12173  fprodmul  12175  prodsnf  12176  fprodm1s  12185  fprodp1s  12186  prodsns  12187  fprodcl2lem  12189  fprodcllemf  12197  fprodabs  12200  fprodap0  12205  fprod2dlemstep  12206  fprodcnv  12209  fprodcom2fi  12210  fprodrec  12213  fproddivapf  12215  fprodsplitf  12216  fprodsplit1f  12218  fprodap0f  12220  fprodle  12224  fprodmodd  12225  pcmpt  12939  pcmptdvds  12941  ctiunctlemudc  13081  ctiunctlemf  13082  ctiunctal  13085  gsumfzfsumlemm  14625  iuncld  14868  fsumcncntop  15320  limcmpted  15416  dvmptfsum  15478  fsumdvdsmul  15744