Theorem nfcsb1v 3861

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	⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfcsb1v

Step	Hyp	Ref	Expression
1		nfcv 2898	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfcsb1 3860	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  Ⅎwnfc 2883  ⦋csb 3837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-sbc 3729  df-csb 3838

This theorem is referenced by:  csbhypf  3865  csbiebt  3866  cbvrabcsfw  3878  cbvralcsf  3879  cbvreucsf  3881  cbvrabcsf  3882  rspc2vd  3885  sbcnestgfw  4361  sbcnestgf  4366  csbnest1g  4372  csbun  4381  csbin  4382  csbdif  4465  csbif  4524  disjors  5068  invdisjrab  5072  disjxiun  5082  disjxun  5083  sbcbr123  5139  eusvnf  5334  reusv2lem4  5343  reusv2  5345  moop2  5456  iunopeqop  5475  iunopeqopOLD  5476  pofun  5557  opeliunxp  5698  opeliun2xp  5699  elrnmpt1  5915  resmptf  6004  csbima12  6044  csbcog  6261  fvmpt2f  6948  fvmpts  6951  fvmptdf  6954  fvmpt2i  6958  fvmptex  6962  fmptco  7082  fmptcof  7083  fmptcos  7084  elabrex  7197  elabrexg  7198  fliftfuns  7269  csbov123  7411  ovmpos  7515  fvmpopr2d  7529  ofmpteq  7654  mpomptsx  8017  dmmpossx  8019  fmpox  8020  el2mpocsbcl  8035  offval22  8038  ovmptss  8043  fmpoco  8045  dfmpo  8052  mpoxeldm  8161  mpocurryd  8219  mpocurryvald  8220  fvmpocurryd  8221  eqerlem  8679  qliftfuns  8751  mptelixpg  8883  boxcutc  8889  xpf1o  9077  iunfi  9253  wdom2d  9495  ixpiunwdom  9505  hsmexlem2  10349  ac6c4  10403  iundom2g  10462  seqof2  14022  rlimcld2  15540  nfsum1  15652  sumeq2ii  15655  summolem3  15676  summolem2a  15677  zsum  15680  fsum  15682  sumss2  15688  fsumcvg2  15689  fsumclf  15700  fsumzcl2  15701  fsumsplitf  15704  sumsnf  15705  sumsns  15712  fsummsnunz  15716  fsumsplitsnun  15717  fsum2dlem  15732  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  fsum00  15761  fsumabs  15764  fsumrlim  15774  fsumo1  15775  o1fsum  15776  fsumiun  15784  infcvgaux1i  15822  nfcprod1  15873  prodeq2ii  15876  prodmolem3  15898  prodmolem2a  15899  zprod  15902  fprod  15906  fprodntriv  15907  prodss  15912  fprodser  15914  fprodcllemf  15923  prodsn  15927  prodsnf  15929  fprodm1s  15935  fprodp1s  15936  prodsns  15937  fprodabs  15939  fprodn0  15944  fprod2dlem  15945  fprodcom2  15949  fproddivf  15952  fprodsplitf  15953  fprodsplit1f  15955  fprodle  15961  fprodmodd  15962  fprodefsum  16060  sumeven  16356  sumodd  16357  pcmpt  16863  pcmptdvds  16865  natpropd  17946  fucpropd  17947  gsummpt1n0  19940  gsumcom2  19950  gsummptnn0fz  19961  dprd2d2  20021  psrass1lem  21912  mpfrcl  22063  coe1fzgsumdlem  22268  gsummoncoe1  22273  gsumply1eq  22274  evl1gsumdlem  22321  mdetralt2  22574  mdetunilem2  22578  madugsum  22608  fiuncmp  23369  ptcld  23578  ptcldmpt  23579  ptclsg  23580  elmptrab  23792  prdsdsf  24332  prdsxmet  24334  fsumcn  24837  fsum2cn  24838  ovolfiniun  25468  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  ovoliunnul  25474  finiunmbl  25511  volfiniun  25514  iundisj  25515  iundisj2  25516  iunmbl  25520  iunmbl2  25524  itgss3  25782  itgfsum  25794  itgabs  25802  limciun  25861  dvmptfsum  25942  dvfsumle  25988  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsum2  26001  itgsubstlem  26015  itgsubst  26016  rlimcnp2  26930  fsumdvdscom  27148  fsumdvdsmul  27158  fsumvma  27176  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  iunxpssiun1  32638  disjorsf  32650  disjabrex  32652  disjabrexf  32653  iundisjf  32659  iundisj2f  32660  disjunsn  32664  suppss2f  32711  2ndresdju  32722  fmptdF  32729  fmptcof2  32730  acunirnmpt2f  32734  aciunf1lem  32735  funcnv4mpt  32741  f1od2  32792  iundisjfi  32869  iundisj2fi  32870  fsumiunle  32902  gsummpt2co  33109  gsummptp1  33118  gsumpart  33124  gsumvsca1  33287  gsumvsca2  33288  rmfsupp2  33299  esumpfinvalf  34220  esum2dlem  34236  esumiun  34238  fiunelros  34318  measiun  34362  voliune  34373  volfiniune  34374  sbcaltop  36163  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  csbttc  36691  bj-sbeqALT  37207  phpreu  37925  finixpnum  37926  ptrest  37940  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  mbfposadd  37988  itgabsnc  38010  ftc1cnnclem  38012  ftc2nc  38023  fsumshftd  39398  riotasv2s  39404  cdleme31sn  40826  cdleme31sn1  40827  cdleme31se2  40829  cdleme32fva  40883  cdleme42b  40924  hlhilset  42380  evl1gprodd  42556  idomnnzgmulnz  42572  deg1gprod  42579  fmpocos  42675  mzpsubst  43180  rabdiophlem2  43230  elnn0rabdioph  43231  dvdsrabdioph  43238  fphpd  43244  monotuz  43369  oddcomabszz  43372  wdom2d2  43463  aomclem6  43487  flcidc  43598  fsumcnf  45452  sumsnd  45457  fiiuncl  45496  eliin2f  45534  disjf1  45613  disjrnmpt2  45618  disjinfi  45622  fmptf  45668  fmptff  45698  iuneqfzuzlem  45764  supxrleubrnmptf  45879  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumiunss  46005  fsumreclf  46006  fsumlessf  46007  fprodexp  46024  fprodabs2  46025  mccllem  46027  fprodcnlem  46029  fprodcn  46030  climeldmeqmpt  46096  climeldmeqmpt3  46117  climinf2mpt  46142  climinfmpt  46143  limsupequzmptf  46159  fprodcncf  46328  dvmptmulf  46365  dvnmptdivc  46366  dvmptfprod  46373  iblsplitf  46398  fourierdlem86  46620  fourierdlem112  46646  sge0f1o  46810  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  hoimbl2  47093  vonn0ioo2  47118  vonn0icc2  47120  csbafv12g  47585  csbaovg  47628  csbafv212g  47667  fsummsndifre  47828  fsumsplitsndif  47829  fsummmodsndifre  47830  fsummmodsnunz  47831  dmmpossx2  48813