Theorem csbeq1a 3066

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

Syntax hints:   → wi 4   = wceq 1353  ⦋csb 3057

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2963  df-csb 3058

This theorem is referenced by:  csbhypf  3095  csbiebt  3096  sbcnestgf  3108  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  rspc2vd  3125  csbing  3342  disjnims  3995  disjiun  3998  sbcbrg  4057  moop2  4251  pofun  4312  eusvnf  4453  opeliunxp  4681  elrnmpt1  4878  resmptf  4957  csbima12g  4989  fvmpts  5594  fvmpt2  5599  mptfvex  5601  fmptco  5682  fmptcof  5683  fmptcos  5684  elabrex  5758  fliftfuns  5798  csbov123g  5912  ovmpos  5997  csbopeq1a  6188  mpomptsx  6197  dmmpossx  6199  fmpox  6200  mpofvex  6203  fmpoco  6216  disjxp1  6236  eqerlem  6565  qliftfuns  6618  mptelixpg  6733  xpf1o  6843  iunfidisj  6944  cc3  7266  seq3f1olemstep  10498  seq3f1olemp  10499  sumeq2  11362  sumfct  11377  sumrbdclem  11380  summodclem3  11383  summodclem2a  11384  zsumdc  11387  fsumgcl  11389  fsum3  11390  isumss  11394  isumss2  11396  fsum3cvg2  11397  fsumzcl2  11408  fsumsplitf  11411  sumsnf  11412  sumsns  11418  fsumsplitsnun  11422  fsum2dlemstep  11437  fsumcnv  11440  fisumcom2  11441  fsumshftm  11448  fisum0diag2  11450  fsummulc2  11451  fsum00  11465  fsumabs  11468  fsumrelem  11474  fsumiun  11480  isumshft  11493  mertenslem2  11539  prodeq2  11560  prodrbdclem  11574  prodmodclem3  11578  prodmodclem2a  11579  zproddc  11582  fprodseq  11586  fprodntrivap  11587  prodfct  11590  prodssdc  11592  fprodmul  11594  prodsnf  11595  fprodm1s  11604  fprodp1s  11605  prodsns  11606  fprodcl2lem  11608  fprodcllemf  11616  fprodabs  11619  fprodap0  11624  fprod2dlemstep  11625  fprodcnv  11628  fprodcom2fi  11629  fprodrec  11632  fproddivapf  11634  fprodsplitf  11635  fprodsplit1f  11637  fprodap0f  11639  fprodle  11643  fprodmodd  11644  pcmpt  12335  pcmptdvds  12337  ctiunctlemudc  12432  ctiunctlemf  12433  ctiunctal  12436  iuncld  13546  fsumcncntop  13987  limcmpted  14063