Theorem csbeq1a 3150

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 3149	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3144	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	eqtr3id 2281	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1398  ⦋csb 3141

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 3046  df-csb 3142

This theorem is referenced by:  csbhypf  3180  csbiebt  3181  sbcnestgf  3193  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  rspc2vd  3210  csbing  3432  ifeqeqxdc  3673  disjnims  4105  invdisjrab  4108  disjiun  4109  sbcbrg  4169  moop2  4373  pofun  4438  eusvnf  4579  opeliunxp  4810  elrnmpt1  5013  resmptf  5093  csbima12g  5128  fvmpts  5760  fvmpt2  5766  mptfvex  5768  fmptco  5848  fmptcof  5849  fmptcos  5850  elabrex  5936  elabrexg  5937  fliftfuns  5977  riotaeqimp  6036  csbov123g  6097  ovmpos  6185  fvmpopr2d  6198  csbopeq1a  6395  mpomptsx  6406  dmmpossx  6408  fmpox  6409  mpofvex  6414  fmpoco  6425  disjxp1  6445  eqerlem  6811  qliftfuns  6866  mptelixpg  6982  xpf1o  7110  iunfidisj  7226  cc3  7598  seq3f1olemstep  10903  seq3f1olemp  10904  sumeq2  12072  sumfct  12087  sumrbdclem  12091  summodclem3  12094  summodclem2a  12095  zsumdc  12098  fsumgcl  12100  fsum3  12101  isumss  12105  isumss2  12107  fsum3cvg2  12108  fsumzcl2  12119  fsumsplitf  12122  sumsnf  12123  sumsns  12129  fsumsplitsnun  12133  fsum2dlemstep  12148  fsumcnv  12151  fisumcom2  12152  fsumshftm  12159  fisum0diag2  12161  fsummulc2  12162  fsum00  12176  fsumabs  12179  fsumrelem  12185  fsumiun  12191  isumshft  12204  mertenslem2  12250  prodeq2  12271  prodrbdclem  12285  prodmodclem3  12289  prodmodclem2a  12290  zproddc  12293  fprodseq  12297  fprodntrivap  12298  prodfct  12301  prodssdc  12303  fprodmul  12305  prodsnf  12306  fprodm1s  12315  fprodp1s  12316  prodsns  12317  fprodcl2lem  12319  fprodcllemf  12327  fprodabs  12330  fprodap0  12335  fprod2dlemstep  12336  fprodcnv  12339  fprodcom2fi  12340  fprodrec  12343  fproddivapf  12345  fprodsplitf  12346  fprodsplit1f  12348  fprodap0f  12350  fprodle  12354  fprodmodd  12355  pcmpt  13069  pcmptdvds  13071  ctiunctlemudc  13275  ctiunctlemf  13276  ctiunctal  13279  gsumfzfsumlemm  14864  iuncld  15109  fsumcncntop  15561  limcmpted  15657  dvmptfsum  15719  fsumdvdsmul  15988