Theorem csbeq1a 3935

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

Syntax hints:   → wi 4   = wceq 1537  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805  df-csb 3922

This theorem is referenced by:  csbhypf  3950  csbiebt  3951  cbvrabcsfw  3965  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  rspc2vd  3972  sbcnestgfw  4444  sbcnestgf  4449  csbun  4464  csbin  4465  csbdif  4547  csbif  4605  disjors  5149  invdisjrab  5153  disjxiun  5163  disjxun  5164  sbcbr123  5220  eusvnf  5410  reusv2lem4  5419  reusv2  5421  moop2  5521  iunopeqop  5540  pofun  5626  opeliunxp  5767  elrnmpt1  5983  resmptf  6068  csbima12  6108  csbcog  6328  fvmpt2f  7030  fvmpts  7032  fvmptdf  7035  fvmpt2i  7039  fvmptex  7043  fmptco  7163  fmptcof  7164  fmptcos  7165  elabrex  7279  elabrexg  7280  fliftfuns  7350  riotaeqimp  7431  csbov123  7492  ovmpos  7598  fvmpopr2d  7612  ofmpteq  7736  csbopeq1a  8091  mpomptsx  8105  dmmpossx  8107  fmpox  8108  el2mpocsbcl  8126  offval22  8129  ovmptss  8134  fmpoco  8136  mpoxeldm  8252  mpocurryd  8310  mpocurryvald  8311  fvmpocurryd  8312  eqerlem  8798  qliftfuns  8862  mptelixpg  8993  boxcutc  8999  xpf1o  9205  iunfi  9411  wdom2d  9649  ixpiunwdom  9659  hsmexlem2  10496  ac6c4  10550  iundom2g  10609  seqof2  14111  rlimcld2  15624  sumeq2ii  15741  summolem3  15762  summolem2a  15763  zsum  15766  fsum  15768  sumss2  15774  fsumcvg2  15775  fsumclf  15786  fsumzcl2  15787  fsumsplitf  15790  sumsnf  15791  fsumsplit1  15793  sumsns  15798  fsummsnunz  15802  fsumsplitsnun  15803  fsum2dlem  15818  fsumcnv  15821  fsumcom2  15822  fsumshftm  15829  fsum0diag2  15831  fsum00  15846  fsumabs  15849  fsumrlim  15859  fsumo1  15860  o1fsum  15861  fsumiun  15869  infcvgaux1i  15905  prodeq2ii  15959  prodmolem3  15981  prodmolem2a  15982  zprod  15985  fprod  15989  fprodntriv  15990  prodss  15995  fprodser  15997  fprodcllemf  16006  prodsn  16010  prodsnf  16012  fprodm1s  16018  fprodp1s  16019  prodsns  16020  fprodabs  16022  fprodn0  16027  fprod2dlem  16028  fprodcnv  16031  fprodcom2  16032  fproddivf  16035  fprodsplitf  16036  fprodsplit1f  16038  fprodle  16044  fprodmodd  16045  fprodefsum  16143  sumeven  16435  sumodd  16436  pcmpt  16939  pcmptdvds  16941  natpropd  18046  fucpropd  18047  gsummpt1n0  20007  gsumcom2  20017  gsummptnn0fz  20028  dprd2d2  20088  psrass1lem  21975  mpfrcl  22132  coe1fzgsumdlem  22328  gsumply1eq  22334  evl1gsumdlem  22381  mdetralt2  22636  mdetunilem2  22640  madugsum  22670  fiuncmp  23433  ptcld  23642  ptcldmpt  23643  ptclsg  23644  elmptrab  23856  prdsdsf  24398  prdsxmet  24400  fsumcn  24913  fsum2cn  24914  ovolfiniun  25555  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  ovoliunnul  25561  finiunmbl  25598  volfiniun  25601  iundisj  25602  iundisj2  25603  iunmbl  25607  iunmbl2  25611  itgss3  25870  itgfsum  25882  itgabs  25890  limciun  25949  dvmptfsum  26033  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlim  26092  dvfsumrlim2  26093  dvfsum2  26095  itgsubstlem  26109  itgsubst  26110  rlimcnp2  27027  fsumdvdscom  27246  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  fsumvma  27275  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  ifeqeqx  32565  disjorsf  32602  disjabrex  32604  disjabrexf  32605  iundisjf  32611  iundisj2f  32612  disjunsn  32616  suppss2f  32657  2ndresdju  32667  fmptdF  32674  fmptcof2  32675  acunirnmpt2f  32679  aciunf1lem  32680  funcnv4mpt  32687  f1od2  32735  iundisjfi  32801  iundisj2fi  32802  fsumiunle  32833  gsummpt2co  33031  gsumpart  33038  gsumvsca1  33205  gsumvsca2  33206  rmfsupp2  33218  esumpfinvalf  34040  esum2dlem  34056  esumiun  34058  fiunelros  34138  measiun  34182  voliune  34193  volfiniune  34194  sbcaltop  35945  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  bj-sbeqALT  36866  rdgssun  37344  finxpreclem2  37356  phpreu  37564  finixpnum  37565  ptrest  37579  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  mbfposadd  37627  itgabsnc  37649  ftc1cnnclem  37651  ftc2nc  37662  fsumshftd  38908  riotasv2s  38914  cdleme31sn  40337  cdleme31sn1  40338  cdleme31se2  40340  cdleme32fva  40394  cdleme42b  40435  hlhilset  41891  evl1gprodd  42074  idomnnzgmulnz  42090  deg1gprod  42097  fmpocos  42229  mzpsubst  42704  rabdiophlem2  42758  elnn0rabdioph  42759  dvdsrabdioph  42766  fphpd  42772  monotuz  42898  oddcomabszz  42901  aomclem6  43016  flcidc  43131  fsumcnf  44921  sumsnd  44926  fiiuncl  44967  eliin2f  45006  disjf1  45090  disjrnmpt2  45095  disjinfi  45099  fmptf  45147  fmptff  45179  iuneqfzuzlem  45249  supxrleubrnmptf  45366  fsummulc1f  45492  fsumnncl  45493  fsumf1of  45495  fsumiunss  45496  fsumreclf  45497  fsumlessf  45498  fsumsermpt  45500  fprodexp  45515  fprodabs2  45516  mccllem  45518  fprodcnlem  45520  fprodcn  45521  climsubmpt  45581  climeldmeqmpt  45589  climfveqmpt  45592  climfveqmpt3  45603  climeldmeqmpt3  45610  climinf2mpt  45635  climinfmpt  45636  limsupequzmptf  45652  fprodcncf  45821  dvmptmulf  45858  dvnmptdivc  45859  dvmptfprod  45866  iblsplitf  45891  fourierdlem86  46113  fourierdlem112  46139  sge0f1o  46303  sge0lempt  46331  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0ltfirpmpt2  46347  sge0isummpt2  46353  sge0xaddlem2  46355  sge0xadd  46356  meadjiun  46387  hoimbl2  46586  vonhoire  46593  vonn0ioo2  46611  vonn0icc2  46613  csbafv12g  47052  csbaovg  47095  csbafv212g  47134  fsummsndifre  47246  fsumsplitsndif  47247  fsummmodsndifre  47248  fsummmodsnunz  47249  opeliun2xp  48057  dmmpossx2  48061