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

Theorem nfcsb1v 3285
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 2574 . 2  |-  F/_ x A
21nfcsb1 3284 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2561   [_csb 3253
This theorem is referenced by:  csbhypf  3288  csbiebt  3289  sbcnestgf  3300  csbnest1g  3305  cbvralcsf  3313  cbvreucsf  3315  cbvrabcsf  3316  csbing  3550  csbifg  3769  disjors  4201  disjxiun  4212  disjxun  4213  sbcbrg  4264  moop2  4454  pofun  4522  eusvnf  4721  reusv2lem4  4730  reusv2  4732  opeliunxp  4932  elrnmpt1  5122  csbima12g  5216  fvmpts  5810  fvmpt2i  5814  fvmptex  5818  fmptco  5904  fmptcof  5905  fmptcos  5906  elabrex  5988  fliftfuns  6039  csbovg  6115  ovmpt2s  6200  mpt2mptsx  6417  dmmpt2ssx  6419  fmpt2x  6420  ovmptss  6431  fmpt2co  6433  dfmpt2  6440  riotasv2s  6599  eqerlem  6940  qliftfuns  6994  mptelixpg  7102  boxcutc  7108  xpf1o  7272  iunfi  7397  wdom2d  7551  ixpiunwdom  7562  hsmexlem2  8312  ac6num  8364  ac6c4  8366  iundom2g  8420  seqof2  11386  rlimcld2  12377  nfsum1  12489  sumeq2w  12491  sumeq2ii  12492  summolem3  12513  summolem2a  12514  zsum  12517  fsum  12519  sumss2  12525  fsumcvg2  12526  sumsn  12539  sumsns  12541  fsum2dlem  12559  fsumcom2  12563  fsumshftm  12569  fsum0diag2  12571  fsum00  12582  fsumabs  12585  fsumrlim  12595  fsumo1  12596  o1fsum  12597  fsumiun  12605  infcvgaux1i  12641  pcmpt  13266  pcmptdvds  13268  natpropd  14178  fucpropd  14179  gsumcom2  15554  dprd2d2  15607  psrass1lem  16447  fiuncmp  17472  ptcld  17650  ptcldmpt  17651  ptclsg  17652  elmptrab  17864  prdsdsf  18402  prdsxmet  18404  fsumcn  18905  fsum2cn  18906  ovolfiniun  19402  ovoliunlem3  19405  ovoliun  19406  ovoliun2  19407  ovoliunnul  19408  finiunmbl  19443  volfiniun  19446  iundisj  19447  iundisj2  19448  iunmbl  19452  iunmbl2  19456  itgss3  19709  itgfsum  19721  itgabs  19729  limciun  19786  dvmptfsum  19864  dvfsumle  19910  dvfsumabs  19912  dvfsumlem1  19915  dvfsumlem2  19916  dvfsumlem3  19917  dvfsumlem4  19918  dvfsumrlim  19920  dvfsumrlim2  19921  dvfsum2  19923  itgsubstlem  19937  itgsubst  19938  mpfrcl  19944  rlimcnp2  20810  fsumdvdscom  20975  fsumdvdsmul  20985  fsumvma  21002  dchrisumlema  21187  dchrisumlem2  21189  dchrisumlem3  21190  disjorsf  24027  disjabrex  24029  disjabrexf  24030  iundisjf  24034  iundisj2f  24035  suppss2f  24054  fmptdF  24074  resmptf  24076  fvmpt2f  24077  fmptcof2  24081  funcnv4mpt  24090  iundisjfi  24157  iundisj2fi  24158  esumpfinvalf  24471  measiun  24577  voliune  24590  volfiniune  24591  sbcung  25129  sbcopg  25131  nfcprod1  25241  prodeq2w  25243  prodeq2ii  25244  prodmolem3  25264  prodmolem2a  25265  zprod  25268  fprod  25272  fprodntriv  25273  prodss  25278  fprodser  25280  prodsn  25291  fprodm1s  25298  fprodp1s  25299  prodsns  25300  fprodabs  25302  fprodefsum  25303  fprodn0  25308  fprod2dlem  25309  fprodcom2  25313  sbcaltop  25831  itgabsnc  26288  ftc1cnnclem  26292  ftc2nc  26303  ofmpteq  26790  mzpsubst  26819  rabdiophlem2  26876  elnn0rabdioph  26877  dvdsrabdioph  26884  fphpd  26891  monotuz  27018  oddcomabszz  27021  wdom2d2  27120  aomclem6  27148  flcidc  27370  fsumcnf  27682  sumsnd  27687  csbafv12g  27991  csbaovg  28034  cdleme31sn  31251  cdleme31sn1  31252  cdleme31se2  31254  cdleme32fva  31308  cdleme42b  31349  hlhilset  32809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-sbc 3164  df-csb 3254
  Copyright terms: Public domain W3C validator