Theorem csbeq1a 3133

Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1a	⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbid 3132	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3127	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	eqtr3id 2276	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1395  ⦋csb 3124

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-sbc 3029  df-csb 3125

This theorem is referenced by:  csbhypf  3163  csbiebt  3164  sbcnestgf  3176  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  rspc2vd  3193  csbing  3411  disjnims  4074  invdisjrab  4077  disjiun  4078  sbcbrg  4138  moop2  4339  pofun  4404  eusvnf  4545  opeliunxp  4776  elrnmpt1  4978  resmptf  5058  csbima12g  5092  fvmpts  5717  fvmpt2  5723  mptfvex  5725  fmptco  5806  fmptcof  5807  fmptcos  5808  elabrex  5890  elabrexg  5891  fliftfuns  5931  riotaeqimp  5988  csbov123g  6049  ovmpos  6137  fvmpopr2d  6150  csbopeq1a  6343  mpomptsx  6354  dmmpossx  6356  fmpox  6357  mpofvex  6362  fmpoco  6373  disjxp1  6393  eqerlem  6724  qliftfuns  6779  mptelixpg  6894  xpf1o  7018  iunfidisj  7129  cc3  7470  seq3f1olemstep  10753  seq3f1olemp  10754  sumeq2  11891  sumfct  11906  sumrbdclem  11909  summodclem3  11912  summodclem2a  11913  zsumdc  11916  fsumgcl  11918  fsum3  11919  isumss  11923  isumss2  11925  fsum3cvg2  11926  fsumzcl2  11937  fsumsplitf  11940  sumsnf  11941  sumsns  11947  fsumsplitsnun  11951  fsum2dlemstep  11966  fsumcnv  11969  fisumcom2  11970  fsumshftm  11977  fisum0diag2  11979  fsummulc2  11980  fsum00  11994  fsumabs  11997  fsumrelem  12003  fsumiun  12009  isumshft  12022  mertenslem2  12068  prodeq2  12089  prodrbdclem  12103  prodmodclem3  12107  prodmodclem2a  12108  zproddc  12111  fprodseq  12115  fprodntrivap  12116  prodfct  12119  prodssdc  12121  fprodmul  12123  prodsnf  12124  fprodm1s  12133  fprodp1s  12134  prodsns  12135  fprodcl2lem  12137  fprodcllemf  12145  fprodabs  12148  fprodap0  12153  fprod2dlemstep  12154  fprodcnv  12157  fprodcom2fi  12158  fprodrec  12161  fproddivapf  12163  fprodsplitf  12164  fprodsplit1f  12166  fprodap0f  12168  fprodle  12172  fprodmodd  12173  pcmpt  12887  pcmptdvds  12889  ctiunctlemudc  13029  ctiunctlemf  13030  ctiunctal  13033  gsumfzfsumlemm  14572  iuncld  14810  fsumcncntop  15262  limcmpted  15358  dvmptfsum  15420  fsumdvdsmul  15686