Theorem csbeq1a 3149

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 3148	. 2 |- [_ x / x ]_ B = B
2		csbeq1 3143	. 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 3140

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 3045  df-csb 3141

This theorem is referenced by:  csbhypf  3179  csbiebt  3180  sbcnestgf  3192  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  rspc2vd  3209  csbing  3430  disjnims  4102  invdisjrab  4105  disjiun  4106  sbcbrg  4166  moop2  4370  pofun  4435  eusvnf  4576  opeliunxp  4807  elrnmpt1  5010  resmptf  5090  csbima12g  5125  fvmpts  5757  fvmpt2  5763  mptfvex  5765  fmptco  5845  fmptcof  5846  fmptcos  5847  elabrex  5932  elabrexg  5933  fliftfuns  5973  riotaeqimp  6030  csbov123g  6091  ovmpos  6179  fvmpopr2d  6192  csbopeq1a  6384  mpomptsx  6395  dmmpossx  6397  fmpox  6398  mpofvex  6403  fmpoco  6414  disjxp1  6434  eqerlem  6800  qliftfuns  6855  mptelixpg  6971  xpf1o  7099  iunfidisj  7215  cc3  7587  seq3f1olemstep  10883  seq3f1olemp  10884  sumeq2  12052  sumfct  12067  sumrbdclem  12071  summodclem3  12074  summodclem2a  12075  zsumdc  12078  fsumgcl  12080  fsum3  12081  isumss  12085  isumss2  12087  fsum3cvg2  12088  fsumzcl2  12099  fsumsplitf  12102  sumsnf  12103  sumsns  12109  fsumsplitsnun  12113  fsum2dlemstep  12128  fsumcnv  12131  fisumcom2  12132  fsumshftm  12139  fisum0diag2  12141  fsummulc2  12142  fsum00  12156  fsumabs  12159  fsumrelem  12165  fsumiun  12171  isumshft  12184  mertenslem2  12230  prodeq2  12251  prodrbdclem  12265  prodmodclem3  12269  prodmodclem2a  12270  zproddc  12273  fprodseq  12277  fprodntrivap  12278  prodfct  12281  prodssdc  12283  fprodmul  12285  prodsnf  12286  fprodm1s  12295  fprodp1s  12296  prodsns  12297  fprodcl2lem  12299  fprodcllemf  12307  fprodabs  12310  fprodap0  12315  fprod2dlemstep  12316  fprodcnv  12319  fprodcom2fi  12320  fprodrec  12323  fproddivapf  12325  fprodsplitf  12326  fprodsplit1f  12328  fprodap0f  12330  fprodle  12334  fprodmodd  12335  pcmpt  13049  pcmptdvds  13051  ctiunctlemudc  13209  ctiunctlemf  13210  ctiunctal  13213  gsumfzfsumlemm  14784  iuncld  15029  fsumcncntop  15481  limcmpted  15577  dvmptfsum  15639  fsumdvdsmul  15908