Theorem csbeq1a 3113

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

Syntax hints:   -> wi 4   = wceq 1375   [_csb 3104

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-sbc 3009  df-csb 3105

This theorem is referenced by:  csbhypf  3143  csbiebt  3144  sbcnestgf  3156  cbvralcsf  3167  cbvrexcsf  3168  cbvreucsf  3169  cbvrabcsf  3170  rspc2vd  3173  csbing  3391  disjnims  4053  invdisjrab  4056  disjiun  4057  sbcbrg  4117  moop2  4317  pofun  4380  eusvnf  4521  opeliunxp  4751  elrnmpt1  4951  resmptf  5031  csbima12g  5065  fvmpts  5685  fvmpt2  5691  mptfvex  5693  fmptco  5774  fmptcof  5775  fmptcos  5776  elabrex  5854  elabrexg  5855  fliftfuns  5895  riotaeqimp  5952  csbov123g  6013  ovmpos  6099  fvmpopr2d  6112  csbopeq1a  6304  mpomptsx  6313  dmmpossx  6315  fmpox  6316  mpofvex  6321  fmpoco  6332  disjxp1  6352  eqerlem  6681  qliftfuns  6736  mptelixpg  6851  xpf1o  6973  iunfidisj  7081  cc3  7422  seq3f1olemstep  10703  seq3f1olemp  10704  sumeq2  11836  sumfct  11851  sumrbdclem  11854  summodclem3  11857  summodclem2a  11858  zsumdc  11861  fsumgcl  11863  fsum3  11864  isumss  11868  isumss2  11870  fsum3cvg2  11871  fsumzcl2  11882  fsumsplitf  11885  sumsnf  11886  sumsns  11892  fsumsplitsnun  11896  fsum2dlemstep  11911  fsumcnv  11914  fisumcom2  11915  fsumshftm  11922  fisum0diag2  11924  fsummulc2  11925  fsum00  11939  fsumabs  11942  fsumrelem  11948  fsumiun  11954  isumshft  11967  mertenslem2  12013  prodeq2  12034  prodrbdclem  12048  prodmodclem3  12052  prodmodclem2a  12053  zproddc  12056  fprodseq  12060  fprodntrivap  12061  prodfct  12064  prodssdc  12066  fprodmul  12068  prodsnf  12069  fprodm1s  12078  fprodp1s  12079  prodsns  12080  fprodcl2lem  12082  fprodcllemf  12090  fprodabs  12093  fprodap0  12098  fprod2dlemstep  12099  fprodcnv  12102  fprodcom2fi  12103  fprodrec  12106  fproddivapf  12108  fprodsplitf  12109  fprodsplit1f  12111  fprodap0f  12113  fprodle  12117  fprodmodd  12118  pcmpt  12832  pcmptdvds  12834  ctiunctlemudc  12974  ctiunctlemf  12975  ctiunctal  12978  gsumfzfsumlemm  14516  iuncld  14754  fsumcncntop  15206  limcmpted  15302  dvmptfsum  15364  fsumdvdsmul  15630