Theorem csbeq1a 3150

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

Syntax hints:   -> wi 4   = wceq 1398   [_csb 3141

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-sbc 3046  df-csb 3142

This theorem is referenced by:  csbhypf  3180  csbiebt  3181  sbcnestgf  3193  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  rspc2vd  3210  csbing  3432  ifeqeqxdc  3674  disjnims  4106  invdisjrab  4109  disjiun  4110  sbcbrg  4170  moop2  4374  pofun  4439  eusvnf  4581  opeliunxp  4812  elrnmpt1  5015  resmptf  5095  csbima12g  5130  fvmpts  5762  fvmpt2  5768  mptfvex  5770  fmptco  5850  fmptcof  5851  fmptcos  5852  elabrex  5938  elabrexg  5939  fliftfuns  5979  riotaeqimp  6038  csbov123g  6099  ovmpos  6187  fvmpopr2d  6200  csbopeq1a  6397  mpomptsx  6408  dmmpossx  6410  fmpox  6411  mpofvex  6416  fmpoco  6427  disjxp1  6447  eqerlem  6813  qliftfuns  6868  mptelixpg  6984  xpf1o  7112  iunfidisj  7228  cc3  7600  seq3f1olemstep  10905  seq3f1olemp  10906  sumeq2  12075  sumfct  12090  sumrbdclem  12094  summodclem3  12097  summodclem2a  12098  zsumdc  12101  fsumgcl  12103  fsum3  12104  isumss  12108  isumss2  12110  fsum3cvg2  12111  fsumzcl2  12122  fsumsplitf  12125  sumsnf  12126  sumsns  12132  fsumsplitsnun  12136  fsum2dlemstep  12151  fsumcnv  12154  fisumcom2  12155  fsumshftm  12162  fisum0diag2  12164  fsummulc2  12165  fsum00  12179  fsumabs  12182  fsumrelem  12188  fsumiun  12194  isumshft  12207  mertenslem2  12253  prodeq2  12274  prodrbdclem  12288  prodmodclem3  12292  prodmodclem2a  12293  zproddc  12296  fprodseq  12300  fprodntrivap  12301  prodfct  12304  prodssdc  12306  fprodmul  12308  prodsnf  12309  fprodm1s  12318  fprodp1s  12319  prodsns  12320  fprodcl2lem  12322  fprodcllemf  12330  fprodabs  12333  fprodap0  12338  fprod2dlemstep  12339  fprodcnv  12342  fprodcom2fi  12343  fprodrec  12346  fproddivapf  12348  fprodsplitf  12349  fprodsplit1f  12351  fprodap0f  12353  fprodle  12357  fprodmodd  12358  pcmpt  13072  pcmptdvds  13074  ctiunctlemudc  13278  ctiunctlemf  13279  ctiunctal  13282  gsumfzfsumlemm  14867  iuncld  15112  fsumcncntop  15564  limcmpted  15660  dvmptfsum  15722  fsumdvdsmul  15991