Theorem csbeq1a 3146

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-sbc 3042  df-csb 3138

This theorem is referenced by:  csbhypf  3176  csbiebt  3177  sbcnestgf  3189  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  rspc2vd  3206  csbing  3427  disjnims  4099  invdisjrab  4102  disjiun  4103  sbcbrg  4163  moop2  4367  pofun  4432  eusvnf  4573  opeliunxp  4804  elrnmpt1  5007  resmptf  5087  csbima12g  5122  fvmpts  5754  fvmpt2  5760  mptfvex  5762  fmptco  5842  fmptcof  5843  fmptcos  5844  elabrex  5929  elabrexg  5930  fliftfuns  5970  riotaeqimp  6027  csbov123g  6088  ovmpos  6176  fvmpopr2d  6189  csbopeq1a  6381  mpomptsx  6392  dmmpossx  6394  fmpox  6395  mpofvex  6400  fmpoco  6411  disjxp1  6431  eqerlem  6797  qliftfuns  6852  mptelixpg  6968  xpf1o  7096  iunfidisj  7212  cc3  7578  seq3f1olemstep  10872  seq3f1olemp  10873  sumeq2  12037  sumfct  12052  sumrbdclem  12056  summodclem3  12059  summodclem2a  12060  zsumdc  12063  fsumgcl  12065  fsum3  12066  isumss  12070  isumss2  12072  fsum3cvg2  12073  fsumzcl2  12084  fsumsplitf  12087  sumsnf  12088  sumsns  12094  fsumsplitsnun  12098  fsum2dlemstep  12113  fsumcnv  12116  fisumcom2  12117  fsumshftm  12124  fisum0diag2  12126  fsummulc2  12127  fsum00  12141  fsumabs  12144  fsumrelem  12150  fsumiun  12156  isumshft  12169  mertenslem2  12215  prodeq2  12236  prodrbdclem  12250  prodmodclem3  12254  prodmodclem2a  12255  zproddc  12258  fprodseq  12262  fprodntrivap  12263  prodfct  12266  prodssdc  12268  fprodmul  12270  prodsnf  12271  fprodm1s  12280  fprodp1s  12281  prodsns  12282  fprodcl2lem  12284  fprodcllemf  12292  fprodabs  12295  fprodap0  12300  fprod2dlemstep  12301  fprodcnv  12304  fprodcom2fi  12305  fprodrec  12308  fproddivapf  12310  fprodsplitf  12311  fprodsplit1f  12313  fprodap0f  12315  fprodle  12319  fprodmodd  12320  pcmpt  13034  pcmptdvds  13036  ctiunctlemudc  13177  ctiunctlemf  13178  ctiunctal  13181  gsumfzfsumlemm  14722  iuncld  14967  fsumcncntop  15419  limcmpted  15515  dvmptfsum  15577  fsumdvdsmul  15846