Theorem csbeq1a 3093

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

Syntax hints:   -> wi 4   = wceq 1364   [_csb 3084

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-sbc 2990  df-csb 3085

This theorem is referenced by:  csbhypf  3123  csbiebt  3124  sbcnestgf  3136  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  rspc2vd  3153  csbing  3370  disjnims  4025  disjiun  4028  sbcbrg  4087  moop2  4284  pofun  4347  eusvnf  4488  opeliunxp  4718  elrnmpt1  4917  resmptf  4996  csbima12g  5030  fvmpts  5639  fvmpt2  5645  mptfvex  5647  fmptco  5728  fmptcof  5729  fmptcos  5730  elabrex  5804  elabrexg  5805  fliftfuns  5845  csbov123g  5960  ovmpos  6046  fvmpopr2d  6059  csbopeq1a  6246  mpomptsx  6255  dmmpossx  6257  fmpox  6258  mpofvex  6263  fmpoco  6274  disjxp1  6294  eqerlem  6623  qliftfuns  6678  mptelixpg  6793  xpf1o  6905  iunfidisj  7012  cc3  7335  seq3f1olemstep  10606  seq3f1olemp  10607  sumeq2  11524  sumfct  11539  sumrbdclem  11542  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsumgcl  11551  fsum3  11552  isumss  11556  isumss2  11558  fsum3cvg2  11559  fsumzcl2  11570  fsumsplitf  11573  sumsnf  11574  sumsns  11580  fsumsplitsnun  11584  fsum2dlemstep  11599  fsumcnv  11602  fisumcom2  11603  fsumshftm  11610  fisum0diag2  11612  fsummulc2  11613  fsum00  11627  fsumabs  11630  fsumrelem  11636  fsumiun  11642  isumshft  11655  mertenslem2  11701  prodeq2  11722  prodrbdclem  11736  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodntrivap  11749  prodfct  11752  prodssdc  11754  fprodmul  11756  prodsnf  11757  fprodm1s  11766  fprodp1s  11767  prodsns  11768  fprodcl2lem  11770  fprodcllemf  11778  fprodabs  11781  fprodap0  11786  fprod2dlemstep  11787  fprodcnv  11790  fprodcom2fi  11791  fprodrec  11794  fproddivapf  11796  fprodsplitf  11797  fprodsplit1f  11799  fprodap0f  11801  fprodle  11805  fprodmodd  11806  pcmpt  12512  pcmptdvds  12514  ctiunctlemudc  12654  ctiunctlemf  12655  ctiunctal  12658  gsumfzfsumlemm  14143  iuncld  14351  fsumcncntop  14803  limcmpted  14899  dvmptfsum  14961  fsumdvdsmul  15227