Theorem csbeq1a 3058

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

Syntax hints:   -> wi 4   = wceq 1348   [_csb 3049

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956  df-csb 3050

This theorem is referenced by:  csbhypf  3087  csbiebt  3088  sbcnestgf  3100  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  rspc2vd  3117  csbing  3334  disjnims  3981  disjiun  3984  sbcbrg  4043  moop2  4236  pofun  4297  eusvnf  4438  opeliunxp  4666  elrnmpt1  4862  resmptf  4941  csbima12g  4972  fvmpts  5574  fvmpt2  5579  mptfvex  5581  fmptco  5662  fmptcof  5663  fmptcos  5664  elabrex  5737  fliftfuns  5777  csbov123g  5891  ovmpos  5976  csbopeq1a  6167  mpomptsx  6176  dmmpossx  6178  fmpox  6179  mpofvex  6182  fmpoco  6195  disjxp1  6215  eqerlem  6544  qliftfuns  6597  mptelixpg  6712  xpf1o  6822  iunfidisj  6923  cc3  7230  seq3f1olemstep  10457  seq3f1olemp  10458  sumeq2  11322  sumfct  11337  sumrbdclem  11340  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumgcl  11349  fsum3  11350  isumss  11354  isumss2  11356  fsum3cvg2  11357  fsumzcl2  11368  fsumsplitf  11371  sumsnf  11372  sumsns  11378  fsumsplitsnun  11382  fsum2dlemstep  11397  fsumcnv  11400  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  fsummulc2  11411  fsum00  11425  fsumabs  11428  fsumrelem  11434  fsumiun  11440  isumshft  11453  mertenslem2  11499  prodeq2  11520  prodrbdclem  11534  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prodfct  11550  prodssdc  11552  fprodmul  11554  prodsnf  11555  fprodm1s  11564  fprodp1s  11565  prodsns  11566  fprodcl2lem  11568  fprodcllemf  11576  fprodabs  11579  fprodap0  11584  fprod2dlemstep  11585  fprodcnv  11588  fprodcom2fi  11589  fprodrec  11592  fproddivapf  11594  fprodsplitf  11595  fprodsplit1f  11597  fprodap0f  11599  fprodle  11603  fprodmodd  11604  pcmpt  12295  pcmptdvds  12297  ctiunctlemudc  12392  ctiunctlemf  12393  ctiunctal  12396  iuncld  12909  fsumcncntop  13350  limcmpted  13426