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

Theorem csbeq1a 3089
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 3088 . 2  |-  [_ x  /  x ]_ B  =  B
2 csbeq1 3084 . 2  |-  ( x  =  A  ->  [_ x  /  x ]_ B  = 
[_ A  /  x ]_ B )
31, 2syl5eqr 2329 1  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   [_csb 3081
This theorem is referenced by:  csbhypf  3116  csbiebt  3117  sbcnestgf  3128  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  csbing  3376  csbifg  3593  disjors  4009  disjxiun  4020  disjxun  4021  sbcbrg  4072  moop2  4261  pofun  4330  eusvnf  4529  reusv2lem4  4538  reusv2  4540  opeliunxp  4740  elrnmpt1  4928  csbima12g  5022  fvmpts  5603  fvmpt2i  5607  fvmptex  5610  fmptco  5691  fmptcof  5692  fmptcos  5693  elabrex  5765  fliftfuns  5813  csbovg  5889  ovmpt2s  5971  csbopeq1a  6173  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  ovmptss  6200  fmpt2co  6202  riotasv2s  6351  eqerlem  6692  qliftfuns  6745  mptelixpg  6853  boxcutc  6859  xpf1o  7023  iunfi  7144  wdom2d  7294  ixpiunwdom  7305  hsmexlem2  8053  ac6num  8106  ac6c4  8108  iundom2g  8162  rlimcld2  12052  sumeq2w  12165  sumeq2ii  12166  summolem3  12187  summolem2a  12188  zsum  12191  fsum  12193  sumss2  12199  fsumcvg2  12200  sumsn  12213  sumsns  12215  fsum2dlem  12233  fsumcnv  12236  fsumcom2  12237  fsumshftm  12243  fsum0diag2  12245  fsum00  12256  fsumabs  12259  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  infcvgaux1i  12315  pcmpt  12940  pcmptdvds  12942  natpropd  13850  fucpropd  13851  gsumcom2  15226  dprd2d2  15279  psrass1lem  16123  fiuncmp  17131  ptcld  17307  ptcldmpt  17308  ptclsg  17309  elmptrab  17522  prdsdsf  17931  prdsxmet  17933  fsumcn  18374  fsum2cn  18375  ovolfiniun  18860  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  ovoliunnul  18866  finiunmbl  18901  volfiniun  18904  iundisj  18905  iundisj2  18906  iunmbl  18910  iunmbl2  18914  itgss3  19169  itgfsum  19181  itgabs  19189  limciun  19244  dvmptfsum  19322  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlim  19378  dvfsumrlim2  19379  dvfsum2  19381  itgsubstlem  19395  itgsubst  19396  mpfrcl  19402  rlimcnp2  20261  fsumdvdscom  20425  fsumdvdsmul  20435  fsumvma  20452  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  ifeqeqx  23034  sbcss12g  23141  suppss2f  23201  fmptdF  23221  resmptf  23223  fvmpt2f  23224  fmptcof2  23229  funcnv4mpt  23237  disjorsf  23357  disjabrex  23359  disjabrexf  23360  iundisjfi  23363  iundisj2fi  23364  iundisjf  23365  iundisj2f  23366  esumpfinvalf  23444  measiun  23545  sbcung  24020  sbcopg  24022  sbcaltop  24515  fprod1s  25325  fprodp1s  25327  ofmpteq  26797  mzpsubst  26826  rabdiophlem2  26883  elnn0rabdioph  26884  dvdsrabdioph  26891  fphpd  26899  monotuz  27026  oddcomabszz  27029  aomclem6  27156  flcidc  27379  fsumcnf  27692  sumsnd  27697  csbafv12g  28000  csbaovg  28040  cdleme31sn  30569  cdleme31sn1  30570  cdleme31se2  30572  cdleme32fva  30626  cdleme42b  30667  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator