Theorem csbeq1a 3156

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   [_csb 3147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-sbc 3052  df-csb 3148

This theorem is used by:  csbhypf  3186  csbiebt  3187  sbcnestgf  3199  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rspc2vd  3216  csbing  3438  ifeqeqxdc  3687  disjnims  4121  invdisjrab  4124  disjiun  4125  sbcbrg  4185  moop2  4392  pofun  4457  eusvnf  4599  opeliunxp  4830  elrnmpt1  5033  resmptf  5113  csbima12g  5148  fvmpts  5783  fvmpt2  5789  mptfvex  5791  fmptco  5874  fmptcof  5875  fmptcos  5876  elabrex  5963  elabrexg  5964  fliftfuns  6004  riotaeqimp  6063  csbov123g  6124  ovmpos  6212  fvmpopr2d  6225  csbopeq1a  6422  mpomptsx  6433  dmmpossx  6435  fmpox  6436  mpofvex  6441  fmpoco  6452  disjxp1  6472  eqerlem  6838  qliftfuns  6893  mptelixpg  7016  xpf1o  7144  iunfidisj  7260  cc3  7634  seq3f1olemstep  10953  seq3f1olemp  10954  sumeq2  12127  sumfct  12142  sumrbdclem  12146  summodclem3  12149  summodclem2a  12150  zsumdc  12153  fsumgcl  12155  fsum3  12156  isumss  12160  isumss2  12162  fsum3cvg2  12163  fsumzcl2  12174  fsumsplitf  12177  sumsnf  12178  sumsns  12184  fsumsplitsnun  12188  fsum2dlemstep  12203  fsumcnv  12206  fisumcom2  12207  fsumshftm  12214  fisum0diag2  12216  fsummulc2  12217  fsum00  12231  fsumabs  12234  fsumrelem  12240  fsumiun  12246  isumshft  12259  mertenslem2  12305  prodeq2  12326  prodrbdclem  12340  prodmodclem3  12344  prodmodclem2a  12345  zproddc  12348  fprodseq  12352  fprodntrivap  12353  prodfct  12356  prodssdc  12358  fprodmul  12360  prodsnf  12361  fprodm1s  12370  fprodp1s  12371  prodsns  12372  fprodcl2lem  12374  fprodcllemf  12382  fprodabs  12385  fprodap0  12390  fprod2dlemstep  12391  fprodcnv  12394  fprodcom2fi  12395  fprodrec  12398  fproddivapf  12400  fprodsplitf  12401  fprodsplit1f  12403  fprodap0f  12405  fprodle  12409  fprodmodd  12410  pcmpt  13124  pcmptdvds  13126  ctiunctlemudc  13330  ctiunctlemf  13331  ctiunctal  13334  gsummptfidmadd  14163  gsumfsum  14925  iuncld  15218  fsumcncntop  15670  limcmpted  15766  dvmptfsum  15828  fsumdvdsmul  16111