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 )

Syntax hints:   -> wi 4   = wceq 1402   [_csb 3147

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 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 theorem 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 referenced by:  csbhypf  3186  csbiebt  3187  sbcnestgf  3199  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rspc2vd  3216  csbing  3438  ifeqeqxdc  3687  disjnims  4119  invdisjrab  4122  disjiun  4123  sbcbrg  4183  moop2  4390  pofun  4455  eusvnf  4597  opeliunxp  4828  elrnmpt1  5031  resmptf  5111  csbima12g  5146  fvmpts  5780  fvmpt2  5786  mptfvex  5788  fmptco  5868  fmptcof  5869  fmptcos  5870  elabrex  5957  elabrexg  5958  fliftfuns  5998  riotaeqimp  6057  csbov123g  6118  ovmpos  6206  fvmpopr2d  6219  csbopeq1a  6416  mpomptsx  6427  dmmpossx  6429  fmpox  6430  mpofvex  6435  fmpoco  6446  disjxp1  6466  eqerlem  6832  qliftfuns  6887  mptelixpg  7010  xpf1o  7138  iunfidisj  7254  cc3  7628  seq3f1olemstep  10934  seq3f1olemp  10935  sumeq2  12108  sumfct  12123  sumrbdclem  12127  summodclem3  12130  summodclem2a  12131  zsumdc  12134  fsumgcl  12136  fsum3  12137  isumss  12141  isumss2  12143  fsum3cvg2  12144  fsumzcl2  12155  fsumsplitf  12158  sumsnf  12159  sumsns  12165  fsumsplitsnun  12169  fsum2dlemstep  12184  fsumcnv  12187  fisumcom2  12188  fsumshftm  12195  fisum0diag2  12197  fsummulc2  12198  fsum00  12212  fsumabs  12215  fsumrelem  12221  fsumiun  12227  isumshft  12240  mertenslem2  12286  prodeq2  12307  prodrbdclem  12321  prodmodclem3  12325  prodmodclem2a  12326  zproddc  12329  fprodseq  12333  fprodntrivap  12334  prodfct  12337  prodssdc  12339  fprodmul  12341  prodsnf  12342  fprodm1s  12351  fprodp1s  12352  prodsns  12353  fprodcl2lem  12355  fprodcllemf  12363  fprodabs  12366  fprodap0  12371  fprod2dlemstep  12372  fprodcnv  12375  fprodcom2fi  12376  fprodrec  12379  fproddivapf  12381  fprodsplitf  12382  fprodsplit1f  12384  fprodap0f  12386  fprodle  12390  fprodmodd  12391  pcmpt  13105  pcmptdvds  13107  ctiunctlemudc  13311  ctiunctlemf  13312  ctiunctal  13315  gsummptfidmadd  14144  gsumfsum  14906  iuncld  15199  fsumcncntop  15651  limcmpted  15747  dvmptfsum  15809  fsumdvdsmul  16088