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

Theorem nfcsb1v 3126
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
nfcsb1v  |-  F/_ x [_ A  /  x ]_ B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2432 . 2  |-  F/_ x A
21nfcsb1 3125 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2419   [_csb 3094
This theorem is referenced by:  csbhypf  3129  csbiebt  3130  sbcnestgf  3141  csbnest1g  3146  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  csbing  3389  csbifg  3606  disjors  4025  disjxiun  4036  disjxun  4037  sbcbrg  4088  moop2  4277  pofun  4346  eusvnf  4545  reusv2lem4  4554  reusv2  4556  opeliunxp  4756  elrnmpt1  4944  csbima12g  5038  fvmpts  5619  fvmpt2i  5623  fvmptex  5626  fmptco  5707  fmptcof  5708  fmptcos  5709  elabrex  5781  fliftfuns  5829  csbovg  5905  ovmpt2s  5987  mpt2mptsx  6203  dmmpt2ssx  6205  fmpt2x  6206  ovmptss  6216  fmpt2co  6218  dfmpt2  6225  riotasv2s  6367  eqerlem  6708  qliftfuns  6761  mptelixpg  6869  boxcutc  6875  xpf1o  7039  iunfi  7160  wdom2d  7310  ixpiunwdom  7321  hsmexlem2  8069  ac6num  8122  ac6c4  8124  iundom2g  8178  rlimcld2  12068  nfsum1  12179  sumeq2w  12181  sumeq2ii  12182  summolem3  12203  summolem2a  12204  zsum  12207  fsum  12209  sumss2  12215  fsumcvg2  12216  sumsn  12229  sumsns  12231  fsum2dlem  12249  fsumcom2  12253  fsumshftm  12259  fsum0diag2  12261  fsum00  12272  fsumabs  12275  fsumrlim  12285  fsumo1  12286  o1fsum  12287  fsumiun  12295  infcvgaux1i  12331  pcmpt  12956  pcmptdvds  12958  natpropd  13866  fucpropd  13867  gsumcom2  15242  dprd2d2  15295  psrass1lem  16139  fiuncmp  17147  ptcld  17323  ptcldmpt  17324  ptclsg  17325  elmptrab  17538  prdsdsf  17947  prdsxmet  17949  fsumcn  18390  fsum2cn  18391  ovolfiniun  18876  ovoliunlem3  18879  ovoliun  18880  ovoliun2  18881  ovoliunnul  18882  finiunmbl  18917  volfiniun  18920  iundisj  18921  iundisj2  18922  iunmbl  18926  iunmbl2  18930  itgss3  19185  itgfsum  19197  itgabs  19205  limciun  19260  dvmptfsum  19338  dvfsumle  19384  dvfsumabs  19386  dvfsumlem1  19389  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlim  19394  dvfsumrlim2  19395  dvfsum2  19397  itgsubstlem  19411  itgsubst  19412  mpfrcl  19418  rlimcnp2  20277  fsumdvdscom  20441  fsumdvdsmul  20451  fsumvma  20468  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  sbcss12g  23157  suppss2f  23216  fmptdF  23236  resmptf  23238  fvmpt2f  23239  fmptcof2  23244  funcnv4mpt  23252  disjorsf  23372  disjabrex  23374  disjabrexf  23375  iundisjfi  23378  iundisj2fi  23379  iundisjf  23380  iundisj2f  23381  esumpfinvalf  23459  sbcung  24035  sbcopg  24037  nfcprod1  24132  cprodeq2w  24134  cprodeq2ii  24135  prodmolem3  24156  prodmolem2a  24157  zprod  24160  fprod  24164  sbcaltop  24587  itgaddnclem2  25010  itgabsnc  25020  fprod1s  25428  fprodp1s  25430  ofmpteq  26900  mzpsubst  26929  rabdiophlem2  26986  elnn0rabdioph  26987  dvdsrabdioph  26994  fphpd  27002  monotuz  27129  oddcomabszz  27132  wdom2d2  27231  aomclem6  27259  flcidc  27482  fsumcnf  27795  sumsnd  27800  csbafv12g  28105  csbaovg  28148  cdleme31sn  31191  cdleme31sn1  31192  cdleme31se2  31194  cdleme32fva  31248  cdleme42b  31289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-sbc 3005  df-csb 3095
  Copyright terms: Public domain W3C validator