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

Theorem csbeq1a 3195
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1a  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )

Proof of Theorem csbeq1a
StepHypRef Expression
1 csbid 3194 . 2  |-  [_ x  /  x ]_ B  =  B
2 csbeq1 3190 . 2  |-  ( x  =  A  ->  [_ x  /  x ]_ B  = 
[_ A  /  x ]_ B )
31, 2syl5eqr 2426 1  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   [_csb 3187
This theorem is referenced by:  csbhypf  3222  csbiebt  3223  sbcnestgf  3234  cbvralcsf  3247  cbvreucsf  3249  cbvrabcsf  3250  csbing  3484  csbifg  3703  disjors  4132  disjxiun  4143  disjxun  4144  sbcbrg  4195  moop2  4385  pofun  4453  eusvnf  4651  reusv2lem4  4660  reusv2  4662  opeliunxp  4862  elrnmpt1  5052  csbima12g  5146  fvmpts  5739  fvmpt2i  5743  fvmptex  5747  fmptco  5833  fmptcof  5834  fmptcos  5835  elabrex  5917  fliftfuns  5968  csbovg  6044  ovmpt2s  6129  csbopeq1a  6332  mpt2mptsx  6346  dmmpt2ssx  6348  fmpt2x  6349  ovmptss  6360  fmpt2co  6362  riotasv2s  6525  eqerlem  6866  qliftfuns  6920  mptelixpg  7028  boxcutc  7034  xpf1o  7198  iunfi  7323  wdom2d  7474  ixpiunwdom  7485  hsmexlem2  8233  ac6num  8285  ac6c4  8287  iundom2g  8341  seqof2  11301  rlimcld2  12292  sumeq2w  12406  sumeq2ii  12407  summolem3  12428  summolem2a  12429  zsum  12432  fsum  12434  sumss2  12440  fsumcvg2  12441  sumsn  12454  sumsns  12456  fsum2dlem  12474  fsumcnv  12477  fsumcom2  12478  fsumshftm  12484  fsum0diag2  12486  fsum00  12497  fsumabs  12500  fsumrlim  12510  fsumo1  12511  o1fsum  12512  fsumiun  12520  infcvgaux1i  12556  pcmpt  13181  pcmptdvds  13183  natpropd  14093  fucpropd  14094  gsumcom2  15469  dprd2d2  15522  psrass1lem  16362  fiuncmp  17382  ptcld  17559  ptcldmpt  17560  ptclsg  17561  elmptrab  17773  prdsdsf  18298  prdsxmet  18300  fsumcn  18764  fsum2cn  18765  ovolfiniun  19257  ovoliunlem3  19260  ovoliun  19261  ovoliun2  19262  ovoliunnul  19263  finiunmbl  19298  volfiniun  19301  iundisj  19302  iundisj2  19303  iunmbl  19307  iunmbl2  19311  itgss3  19566  itgfsum  19578  itgabs  19586  limciun  19641  dvmptfsum  19719  dvfsumle  19765  dvfsumabs  19767  dvfsumlem1  19770  dvfsumlem2  19771  dvfsumlem3  19772  dvfsumlem4  19773  dvfsumrlim  19775  dvfsumrlim2  19776  dvfsum2  19778  itgsubstlem  19792  itgsubst  19793  mpfrcl  19799  rlimcnp2  20665  fsumdvdscom  20830  fsumdvdsmul  20840  fsumvma  20857  dchrisumlema  21042  dchrisumlem2  21044  dchrisumlem3  21045  ifeqeqx  23838  disjorsf  23859  disjabrex  23861  disjabrexf  23862  iundisjf  23865  iundisj2f  23866  suppss2f  23885  fmptdF  23904  resmptf  23906  fvmpt2f  23907  fmptcof2  23911  funcnv4mpt  23919  iundisjfi  23983  iundisj2fi  23984  esumpfinvalf  24255  measiun  24359  voliune  24372  volfiniune  24373  sbcung  24896  sbcopg  24898  prodeq2w  25010  prodeq2ii  25011  prodmolem3  25031  prodmolem2a  25032  zprod  25035  fprod  25039  fprodntriv  25040  prodss  25045  fprodser  25047  prodsn  25058  fprodm1s  25065  fprodp1s  25066  prodsns  25067  fprodabs  25069  fprodefsum  25070  fprodn0  25075  sbcaltop  25533  itgaddnclem2  25957  itgabsnc  25967  ofmpteq  26460  mzpsubst  26489  rabdiophlem2  26546  elnn0rabdioph  26547  dvdsrabdioph  26554  fphpd  26561  monotuz  26688  oddcomabszz  26691  aomclem6  26818  flcidc  27041  fsumcnf  27353  sumsnd  27358  csbafv12g  27663  csbaovg  27706  cdleme31sn  30545  cdleme31sn1  30546  cdleme31se2  30548  cdleme32fva  30602  cdleme42b  30643  hlhilset  32103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-sbc 3098  df-csb 3188
  Copyright terms: Public domain W3C validator