Theorem csbeq1a 3068

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

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

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 2965  df-csb 3060

This theorem is referenced by:  csbhypf  3097  csbiebt  3098  sbcnestgf  3110  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  rspc2vd  3127  csbing  3344  disjnims  3997  disjiun  4000  sbcbrg  4059  moop2  4253  pofun  4314  eusvnf  4455  opeliunxp  4683  elrnmpt1  4880  resmptf  4959  csbima12g  4991  fvmpts  5596  fvmpt2  5601  mptfvex  5603  fmptco  5684  fmptcof  5685  fmptcos  5686  elabrex  5760  elabrexg  5761  fliftfuns  5801  csbov123g  5915  ovmpos  6000  csbopeq1a  6191  mpomptsx  6200  dmmpossx  6202  fmpox  6203  mpofvex  6206  fmpoco  6219  disjxp1  6239  eqerlem  6568  qliftfuns  6621  mptelixpg  6736  xpf1o  6846  iunfidisj  6947  cc3  7269  seq3f1olemstep  10503  seq3f1olemp  10504  sumeq2  11369  sumfct  11384  sumrbdclem  11387  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsumgcl  11396  fsum3  11397  isumss  11401  isumss2  11403  fsum3cvg2  11404  fsumzcl2  11415  fsumsplitf  11418  sumsnf  11419  sumsns  11425  fsumsplitsnun  11429  fsum2dlemstep  11444  fsumcnv  11447  fisumcom2  11448  fsumshftm  11455  fisum0diag2  11457  fsummulc2  11458  fsum00  11472  fsumabs  11475  fsumrelem  11481  fsumiun  11487  isumshft  11500  mertenslem2  11546  prodeq2  11567  prodrbdclem  11581  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodntrivap  11594  prodfct  11597  prodssdc  11599  fprodmul  11601  prodsnf  11602  fprodm1s  11611  fprodp1s  11612  prodsns  11613  fprodcl2lem  11615  fprodcllemf  11623  fprodabs  11626  fprodap0  11631  fprod2dlemstep  11632  fprodcnv  11635  fprodcom2fi  11636  fprodrec  11639  fproddivapf  11641  fprodsplitf  11642  fprodsplit1f  11644  fprodap0f  11646  fprodle  11650  fprodmodd  11651  pcmpt  12343  pcmptdvds  12345  ctiunctlemudc  12440  ctiunctlemf  12441  ctiunctal  12444  iuncld  13654  fsumcncntop  14095  limcmpted  14171