Theorem csbeq1a 3860

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbhypf  3874  csbiebt  3875  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  rspc2vd  3894  sbcnestgfw  4378  sbcnestgf  4383  csbun  4398  csbin  4399  csbdif  4480  csbif  4539  disjors  5085  invdisjrab  5089  disjxiun  5099  disjxun  5100  sbcbr123  5159  eusvnf  5353  reusv2lem4  5362  reusv2  5364  moop2  5473  iunopeqop  5493  iunopeqopOLD  5494  pofun  5576  opeliunxp  5717  opeliun2xp  5718  elrnmpt1  5941  resmptf  6030  csbima12  6075  csbcog  6300  fvmpt2f  6994  fvmpts  6997  fvmptdf  7000  fvmpt2i  7004  fvmptex  7008  fmptco  7130  fmptcof  7131  fmptcos  7132  elabrex  7246  elabrexg  7247  fliftfuns  7322  riotaeqimp  7403  csbov123  7464  ovmpos  7568  fvmpopr2d  7582  ofmpteq  7716  csbopeq1a  8061  mpomptsx  8075  dmmpossx  8077  fmpox  8078  el2mpocsbcl  8096  offval22  8099  ovmptss  8104  fmpoco  8106  mpoxeldm  8228  mpocurryd  8286  mpocurryvald  8287  fvmpocurryd  8288  eqerlem  8753  qliftfuns  8825  mptelixpg  8963  boxcutc  8969  xpf1o  9158  iunfi  9332  wdom2d  9574  ixpiunwdom  9584  hsmexlem2  10505  ac6c4  10559  iundom2g  10624  seqof2  14203  rlimcld2  15745  sumeq2ii  15860  summolem3  15880  summolem2a  15881  zsum  15884  fsum  15886  sumss2  15892  fsumcvg2  15893  fsumclf  15904  fsumzcl2  15905  fsumsplitf  15908  sumsnf  15909  fsumsplit1  15911  sumsns  15916  fsummsnunz  15920  fsumsplitsnun  15921  fsum2dlem  15936  fsumcnv  15939  fsumcom2  15940  fsumshftm  15947  fsum0diag2  15949  fsum00  15965  fsumabs  15968  fsumrlim  15978  fsumo1  15979  o1fsum  15980  fsumiun  15988  infcvgaux1i  16026  prodeq2ii  16080  prodmolem3  16100  prodmolem2a  16101  zprod  16104  fprod  16108  fprodntriv  16109  prodss  16114  fprodser  16116  fprodcllemf  16125  prodsn  16129  prodsnf  16131  fprodm1s  16137  fprodp1s  16138  prodsns  16139  fprodabs  16141  fprodn0  16146  fprod2dlem  16147  fprodcnv  16150  fprodcom2  16151  fproddivf  16154  fprodsplitf  16155  fprodsplit1f  16157  fprodle  16163  fprodmodd  16164  fprodefsum  16261  sumeven  16557  sumodd  16558  pcmpt  17070  pcmptdvds  17072  natpropd  18154  fucpropd  18155  gsummpt1n0  20179  gsumcom2  20189  gsummptnn0fz  20200  dprd2d2  20260  psrass1lem  22241  mpfrcl  22394  coe1fzgsumdlem  22621  gsumply1eq  22627  evl1gsumdlem  22674  mdetralt2  22924  mdetunilem2  22928  madugsum  22958  fiuncmp  23722  ptcld  23932  ptcldmpt  23933  ptclsg  23934  elmptrab  24146  prdsdsf  24686  prdsxmet  24688  fsumcn  25191  fsum2cn  25192  ovolfiniun  25822  ovoliunlem3  25825  ovoliun  25826  ovoliun2  25827  ovoliunnul  25828  finiunmbl  25865  volfiniun  25868  iundisj  25869  iundisj2  25870  iunmbl  25874  iunmbl2  25878  itgss3  26135  itgfsum  26147  itgabs  26155  limciun  26214  dvmptfsum  26295  dvfsumle  26341  dvfsumabs  26343  dvfsumlem1  26346  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsumrlim  26351  dvfsumrlim2  26352  dvfsum2  26354  itgsubstlem  26368  itgsubst  26369  rlimcnp2  27294  fsumdvdscom  27512  fsumdvdsmul  27522  fsumvma  27540  dchrisumlema  27815  dchrisumlem2  27817  dchrisumlem3  27818  ifeqeqx  33180  iunxpssiun1  33204  disjorsf  33216  disjabrex  33218  disjabrexf  33219  iundisjf  33225  iundisj2f  33226  disjunsn  33230  suppss2f  33274  2ndresdju  33285  fmptdf2  33292  fmptcof2  33293  acunirnmpt2f  33297  aciunf1lem  33298  funcnv4mpt  33304  f1od2  33353  iundisjfi  33430  iundisj2fi  33431  fsumiunle  33462  gsummpt2co  33651  gsummptp1  33660  gsumpart  33666  gsumvsca1  33829  gsumvsca2  33830  rmfsupp2  33840  esumpfinvalf  34750  esum2dlem  34766  esumiun  34768  fiunelros  34849  measiun  34893  voliune  34904  volfiniune  34905  sbcaltop  36788  weiunpo  37295  weiunso  37296  weiunfr  37297  weiunse  37298  csbttc  37339  bj-sbeqALT  37854  rdgssun  38344  finxpreclem2  38356  phpreu  38570  finixpnum  38571  ptrest  38580  poimirlem23  38604  poimirlem24  38605  poimirlem25  38606  poimirlem26  38607  poimirlem27  38608  poimirlem28  38609  mbfposadd  38628  itgabsnc  38650  ftc1cnnclem  38652  ftc2nc  38663  fsumshftd  40052  riotasv2s  40058  cdleme31sn  41480  cdleme31sn1  41481  cdleme31se2  41483  cdleme32fva  41537  cdleme42b  41578  hlhilset  43034  evl1gprodd  43210  idomnnzgmulnz  43226  deg1gprod  43233  fmpocos  43330  mzpsubst  43802  rabdiophlem2  43852  elnn0rabdioph  43853  dvdsrabdioph  43860  fphpd  43866  monotuz  43991  oddcomabszz  43994  aomclem6  44104  flcidc  44215  fsumcnf  46081  sumsnd  46086  fiiuncl  46125  eliin2f  46162  disjf1  46241  disjrnmpt2  46246  disjinfi  46250  fmptf  46294  fmptff  46324  iuneqfzuzlem  46389  supxrleubrnmptf  46504  fsummulc1f  46626  fsumnncl  46627  fsumf1of  46629  fsumiunss  46630  fsumreclf  46631  fsumlessf  46632  fsumsermpt  46634  fprodexp  46649  fprodabs2  46650  mccllem  46652  fprodcnlem  46654  fprodcn  46655  climsubmpt  46713  climeldmeqmpt  46721  climfveqmpt  46724  climfveqmpt3  46735  climeldmeqmpt3  46742  climinf2mpt  46767  climinfmpt  46768  limsupequzmptf  46784  fprodcncf  46953  dvmptmulf  46990  dvnmptdivc  46991  dvmptfprod  46998  iblsplitf  47023  fourierdlem86  47245  fourierdlem112  47271  sge0f1o  47435  sge0lempt  47463  sge0iunmptlemfi  47466  sge0iunmptlemre  47468  sge0iunmpt  47471  sge0ltfirpmpt2  47479  sge0isummpt2  47485  sge0xaddlem2  47487  sge0xadd  47488  meadjiun  47519  hoimbl2  47718  vonhoire  47725  vonn0ioo2  47743  vonn0icc2  47745  csbafv12g  48250  csbaovg  48293  csbafv212g  48332  fsummsndifre  48493  fsumsplitsndif  48494  fsummmodsndifre  48495  fsummmodsnunz  48496  dmmpossx2  49492