Theorem csbeq1a 3134

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

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

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 3030  df-csb 3126

This theorem is referenced by:  csbhypf  3164  csbiebt  3165  sbcnestgf  3177  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  rspc2vd  3194  csbing  3412  disjnims  4077  invdisjrab  4080  disjiun  4081  sbcbrg  4141  moop2  4342  pofun  4407  eusvnf  4548  opeliunxp  4779  elrnmpt1  4981  resmptf  5061  csbima12g  5095  fvmpts  5720  fvmpt2  5726  mptfvex  5728  fmptco  5809  fmptcof  5810  fmptcos  5811  elabrex  5893  elabrexg  5894  fliftfuns  5934  riotaeqimp  5991  csbov123g  6052  ovmpos  6140  fvmpopr2d  6153  csbopeq1a  6346  mpomptsx  6357  dmmpossx  6359  fmpox  6360  mpofvex  6365  fmpoco  6376  disjxp1  6396  eqerlem  6728  qliftfuns  6783  mptelixpg  6898  xpf1o  7025  iunfidisj  7139  cc3  7480  seq3f1olemstep  10769  seq3f1olemp  10770  sumeq2  11913  sumfct  11928  sumrbdclem  11931  summodclem3  11934  summodclem2a  11935  zsumdc  11938  fsumgcl  11940  fsum3  11941  isumss  11945  isumss2  11947  fsum3cvg2  11948  fsumzcl2  11959  fsumsplitf  11962  sumsnf  11963  sumsns  11969  fsumsplitsnun  11973  fsum2dlemstep  11988  fsumcnv  11991  fisumcom2  11992  fsumshftm  11999  fisum0diag2  12001  fsummulc2  12002  fsum00  12016  fsumabs  12019  fsumrelem  12025  fsumiun  12031  isumshft  12044  mertenslem2  12090  prodeq2  12111  prodrbdclem  12125  prodmodclem3  12129  prodmodclem2a  12130  zproddc  12133  fprodseq  12137  fprodntrivap  12138  prodfct  12141  prodssdc  12143  fprodmul  12145  prodsnf  12146  fprodm1s  12155  fprodp1s  12156  prodsns  12157  fprodcl2lem  12159  fprodcllemf  12167  fprodabs  12170  fprodap0  12175  fprod2dlemstep  12176  fprodcnv  12179  fprodcom2fi  12180  fprodrec  12183  fproddivapf  12185  fprodsplitf  12186  fprodsplit1f  12188  fprodap0f  12190  fprodle  12194  fprodmodd  12195  pcmpt  12909  pcmptdvds  12911  ctiunctlemudc  13051  ctiunctlemf  13052  ctiunctal  13055  gsumfzfsumlemm  14594  iuncld  14832  fsumcncntop  15284  limcmpted  15380  dvmptfsum  15442  fsumdvdsmul  15708