MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbeq1a Structured version   Visualization version   GIF version

Theorem csbeq1a 3737
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1a (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)

Proof of Theorem csbeq1a
StepHypRef Expression
1 csbid 3736 . 2 𝑥 / 𝑥𝐵 = 𝐵
2 csbeq1 3731 . 2 (𝑥 = 𝐴𝑥 / 𝑥𝐵 = 𝐴 / 𝑥𝐵)
31, 2syl5eqr 2854 1 (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  csb 3728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-sbc 3634  df-csb 3729
This theorem is referenced by:  csbhypf  3747  csbiebt  3748  cbvralcsf  3760  cbvreucsf  3762  cbvrabcsf  3763  sbcnestgf  4192  csbun  4207  csbin  4208  csbif  4334  disjors  4827  invdisjrab  4831  disjxiun  4841  disjxun  4842  sbcbr123  4898  eusvnf  5061  reusv2lem4  5070  reusv2  5072  moop2  5155  iunopeqop  5176  pofun  5248  opeliunxp  5370  elrnmpt1  5575  resmptf  5656  csbima12  5693  fvmpt2f  6504  fvmpts  6506  fvmpt2i  6511  fvmptex  6515  fmptco  6619  fmptcof  6620  fmptcos  6621  elabrex  6725  fliftfuns  6788  riotaeqimp  6858  csbov123  6915  ovmpt2s  7014  ofmpteq  7146  csbopeq1a  7453  mpt2mptsx  7466  dmmpt2ssx  7468  fmpt2x  7469  el2mpt2csbcl  7483  offval22  7487  ovmptss  7492  fmpt2co  7494  mpt2xeldm  7572  mpt2curryd  7630  mpt2curryvald  7631  fvmpt2curryd  7632  eqerlem  8013  qliftfuns  8069  mptelixpg  8182  boxcutc  8188  xpf1o  8361  iunfi  8493  wdom2d  8724  ixpiunwdom  8735  hsmexlem2  9534  ac6num  9586  ac6c4  9588  iundom2g  9647  seqof2  13082  rlimcld2  14532  sumeq2ii  14646  summolem3  14668  summolem2a  14669  zsum  14672  fsum  14674  sumss2  14680  fsumcvg2  14681  fsumzcl2  14692  fsumsplitf  14695  sumsnf  14696  sumsn  14698  sumsns  14702  fsummsnunz  14706  fsumsplitsnun  14707  fsummsnunzOLD  14708  fsumsplitsnunOLD  14709  fsum2dlem  14724  fsumcnv  14727  fsumcom2  14728  fsumshftm  14735  fsum0diag2  14737  fsum00  14752  fsumabs  14755  fsumrlim  14765  fsumo1  14766  o1fsum  14767  fsumiun  14775  infcvgaux1i  14811  prodeq2ii  14864  prodmolem3  14884  prodmolem2a  14885  zprod  14888  fprod  14892  fprodntriv  14893  prodss  14898  fprodser  14900  fprodcllemf  14909  prodsn  14913  prodsnf  14915  fprodm1s  14921  fprodp1s  14922  prodsns  14923  fprodabs  14925  fprodn0  14930  fprod2dlem  14931  fprodcnv  14934  fprodcom2  14935  fproddivf  14938  fprodsplitf  14939  fprodsplit1f  14941  fprodle  14947  fprodmodd  14948  fprodefsum  15045  sumeven  15330  sumodd  15331  pcmpt  15813  pcmptdvds  15815  natpropd  16840  fucpropd  16841  gsummpt1n0  18565  gsumcom2  18575  gsummptnn0fz  18583  gsummptnn0fzOLD  18584  dprd2d2  18645  psrass1lem  19586  mpfrcl  19726  coe1fzgsumdlem  19879  gsumply1eq  19883  evl1gsumdlem  19928  mdetralt2  20626  mdetunilem2  20630  madugsum  20660  fiuncmp  21421  ptcld  21630  ptcldmpt  21631  ptclsg  21632  elmptrab  21844  prdsdsf  22385  prdsxmet  22387  fsumcn  22886  fsum2cn  22887  ovolfiniun  23482  ovoliunlem3  23485  ovoliun  23486  ovoliun2  23487  ovoliunnul  23488  finiunmbl  23525  volfiniun  23528  iundisj  23529  iundisj2  23530  iunmbl  23534  iunmbl2  23538  itgss3  23795  itgfsum  23807  itgabs  23815  limciun  23872  dvmptfsum  23952  dvfsumle  23998  dvfsumabs  24000  dvfsumlem1  24003  dvfsumlem2  24004  dvfsumlem3  24005  dvfsumlem4  24006  dvfsumrlim  24008  dvfsumrlim2  24009  dvfsum2  24011  itgsubstlem  24025  itgsubst  24026  rlimcnp2  24907  fsumdvdscom  25125  fsumdvdsmul  25135  fsumvma  25152  dchrisumlema  25391  dchrisumlem2  25393  dchrisumlem3  25394  rspc2vd  27440  ifeqeqx  29686  disjorsf  29718  disjabrex  29720  disjabrexf  29721  iundisjf  29727  iundisj2f  29728  disjunsn  29732  suppss2f  29766  fmptdF  29783  fmptcof2  29784  acunirnmpt2f  29788  aciunf1lem  29789  funcnv4mpt  29797  f1od2  29826  iundisjfi  29882  iundisj2fi  29883  fsumiunle  29902  gsummpt2co  30105  gsumvsca1  30107  gsumvsca2  30108  esumpfinvalf  30463  esum2dlem  30479  esumiun  30481  fiunelros  30562  measiun  30606  voliune  30617  volfiniune  30618  sbcaltop  32409  bj-sbeqALT  33203  csbdif  33488  finxpreclem2  33543  phpreu  33706  finixpnum  33707  ptrest  33721  poimirlem23  33745  poimirlem24  33746  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  poimirlem28  33750  mbfposadd  33769  itgabsnc  33791  ftc1cnnclem  33795  ftc2nc  33806  fsumshftd  34731  riotasv2s  34737  cdleme31sn  36161  cdleme31sn1  36162  cdleme31se2  36164  cdleme32fva  36218  cdleme42b  36259  hlhilset  37715  mzpsubst  37813  rabdiophlem2  37868  elnn0rabdioph  37869  dvdsrabdioph  37876  fphpd  37882  monotuz  38007  oddcomabszz  38010  aomclem6  38130  flcidc  38245  csbcog  38441  csbingOLD  39549  fsumcnf  39674  sumsnd  39679  elabrexg  39700  fiiuncl  39727  eliin2f  39779  disjf1  39858  disjrnmpt2  39864  disjinfi  39869  fmptf  39932  iuneqfzuzlem  40030  supxrleubrnmptf  40159  fsumclf  40281  fsummulc1f  40282  fsumnncl  40283  fsumsplit1  40284  fsumf1of  40286  fsumiunss  40287  fsumreclf  40288  fsumlessf  40289  fsumsermpt  40291  fprodexp  40306  fprodabs2  40307  mccllem  40309  fprodcnlem  40311  fprodcn  40312  climsubmpt  40372  climeldmeqmpt  40380  climfveqmpt  40383  climfveqmpt3  40394  climeldmeqmpt3  40401  climinf2mpt  40426  climinfmpt  40427  limsupequzmptf  40443  fprodcncf  40594  dvmptmulf  40632  dvnmptdivc  40633  dvmptfprod  40640  iblsplitf  40665  fourierdlem86  40888  fourierdlem112  40914  sge0f1o  41078  sge0lempt  41106  sge0iunmptlemfi  41109  sge0iunmptlemre  41111  sge0iunmpt  41114  sge0ltfirpmpt2  41122  sge0isummpt2  41128  sge0xaddlem2  41130  sge0xadd  41131  meadjiun  41162  hoimbl2  41361  vonhoire  41368  vonn0ioo2  41386  vonn0icc2  41388  csbafv12g  41726  csbaovg  41769  csbafv212g  41808  fsummsndifre  41917  fsumsplitsndif  41918  fsummmodsndifre  41919  fsummmodsnunz  41920  opeliun2xp  42679  dmmpt2ssx2  42683
  Copyright terms: Public domain W3C validator