Theorem csbeq1a 3852

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

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbhypf  3866  csbiebt  3867  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  rspc2vd  3886  sbcnestgfw  4362  sbcnestgf  4367  csbun  4382  csbin  4383  csbdif  4466  csbif  4525  disjors  5069  invdisjrab  5073  disjxiun  5083  disjxun  5084  sbcbr123  5140  eusvnf  5335  reusv2lem4  5344  reusv2  5346  moop2  5457  iunopeqop  5476  pofun  5557  opeliunxp  5698  opeliun2xp  5699  elrnmpt1  5916  resmptf  6005  csbima12  6045  csbcog  6262  fvmpt2f  6949  fvmpts  6952  fvmptdf  6955  fvmpt2i  6959  fvmptex  6963  fmptco  7083  fmptcof  7084  fmptcos  7085  elabrex  7197  elabrexg  7198  fliftfuns  7269  riotaeqimp  7350  csbov123  7411  ovmpos  7515  fvmpopr2d  7529  ofmpteq  7654  csbopeq1a  8003  mpomptsx  8017  dmmpossx  8019  fmpox  8020  el2mpocsbcl  8035  offval22  8038  ovmptss  8043  fmpoco  8045  mpoxeldm  8161  mpocurryd  8219  mpocurryvald  8220  fvmpocurryd  8221  eqerlem  8679  qliftfuns  8751  mptelixpg  8883  boxcutc  8889  xpf1o  9077  iunfi  9253  wdom2d  9495  ixpiunwdom  9505  hsmexlem2  10349  ac6c4  10403  iundom2g  10462  seqof2  14022  rlimcld2  15540  sumeq2ii  15655  summolem3  15676  summolem2a  15677  zsum  15680  fsum  15682  sumss2  15688  fsumcvg2  15689  fsumclf  15700  fsumzcl2  15701  fsumsplitf  15704  sumsnf  15705  fsumsplit1  15707  sumsns  15712  fsummsnunz  15716  fsumsplitsnun  15717  fsum2dlem  15732  fsumcnv  15735  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  fsum00  15761  fsumabs  15764  fsumrlim  15774  fsumo1  15775  o1fsum  15776  fsumiun  15784  infcvgaux1i  15822  prodeq2ii  15876  prodmolem3  15898  prodmolem2a  15899  zprod  15902  fprod  15906  fprodntriv  15907  prodss  15912  fprodser  15914  fprodcllemf  15923  prodsn  15927  prodsnf  15929  fprodm1s  15935  fprodp1s  15936  prodsns  15937  fprodabs  15939  fprodn0  15944  fprod2dlem  15945  fprodcnv  15948  fprodcom2  15949  fproddivf  15952  fprodsplitf  15953  fprodsplit1f  15955  fprodle  15961  fprodmodd  15962  fprodefsum  16060  sumeven  16356  sumodd  16357  pcmpt  16863  pcmptdvds  16865  natpropd  17946  fucpropd  17947  gsummpt1n0  19940  gsumcom2  19950  gsummptnn0fz  19961  dprd2d2  20021  psrass1lem  21912  mpfrcl  22063  coe1fzgsumdlem  22268  gsumply1eq  22274  evl1gsumdlem  22321  mdetralt2  22574  mdetunilem2  22578  madugsum  22608  fiuncmp  23369  ptcld  23578  ptcldmpt  23579  ptclsg  23580  elmptrab  23792  prdsdsf  24332  prdsxmet  24334  fsumcn  24837  fsum2cn  24838  ovolfiniun  25468  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  ovoliunnul  25474  finiunmbl  25511  volfiniun  25514  iundisj  25515  iundisj2  25516  iunmbl  25520  iunmbl2  25524  itgss3  25782  itgfsum  25794  itgabs  25802  limciun  25861  dvmptfsum  25942  dvfsumle  25988  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsum2  26001  itgsubstlem  26015  itgsubst  26016  rlimcnp2  26930  fsumdvdscom  27148  fsumdvdsmul  27158  fsumvma  27176  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  ifeqeqx  32612  iunxpssiun1  32638  disjorsf  32650  disjabrex  32652  disjabrexf  32653  iundisjf  32659  iundisj2f  32660  disjunsn  32664  suppss2f  32711  2ndresdju  32722  fmptdF  32729  fmptcof2  32730  acunirnmpt2f  32734  aciunf1lem  32735  funcnv4mpt  32741  f1od2  32792  iundisjfi  32869  iundisj2fi  32870  fsumiunle  32902  gsummpt2co  33109  gsummptp1  33118  gsumpart  33124  gsumvsca1  33287  gsumvsca2  33288  rmfsupp2  33299  esumpfinvalf  34220  esum2dlem  34236  esumiun  34238  fiunelros  34318  measiun  34362  voliune  34373  volfiniune  34374  sbcaltop  36163  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  csbttc  36691  bj-sbeqALT  37207  rdgssun  37694  finxpreclem2  37706  phpreu  37925  finixpnum  37926  ptrest  37940  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  mbfposadd  37988  itgabsnc  38010  ftc1cnnclem  38012  ftc2nc  38023  fsumshftd  39398  riotasv2s  39404  cdleme31sn  40826  cdleme31sn1  40827  cdleme31se2  40829  cdleme32fva  40883  cdleme42b  40924  hlhilset  42380  evl1gprodd  42556  idomnnzgmulnz  42572  deg1gprod  42579  fmpocos  42675  mzpsubst  43180  rabdiophlem2  43230  elnn0rabdioph  43231  dvdsrabdioph  43238  fphpd  43244  monotuz  43369  oddcomabszz  43372  aomclem6  43487  flcidc  43598  fsumcnf  45452  sumsnd  45457  fiiuncl  45496  eliin2f  45534  disjf1  45613  disjrnmpt2  45618  disjinfi  45622  fmptf  45668  fmptff  45698  iuneqfzuzlem  45764  supxrleubrnmptf  45879  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumiunss  46005  fsumreclf  46006  fsumlessf  46007  fsumsermpt  46009  fprodexp  46024  fprodabs2  46025  mccllem  46027  fprodcnlem  46029  fprodcn  46030  climsubmpt  46088  climeldmeqmpt  46096  climfveqmpt  46099  climfveqmpt3  46110  climeldmeqmpt3  46117  climinf2mpt  46142  climinfmpt  46143  limsupequzmptf  46159  fprodcncf  46328  dvmptmulf  46365  dvnmptdivc  46366  dvmptfprod  46373  iblsplitf  46398  fourierdlem86  46620  fourierdlem112  46646  sge0f1o  46810  sge0lempt  46838  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  meadjiun  46894  hoimbl2  47093  vonhoire  47100  vonn0ioo2  47118  vonn0icc2  47120  csbafv12g  47579  csbaovg  47622  csbafv212g  47661  fsummsndifre  47822  fsumsplitsndif  47823  fsummmodsndifre  47824  fsummmodsnunz  47825  dmmpossx2  48807