Theorem nfcsb1v 3875

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 2899	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfcsb1 3874	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  Ⅎwnfc 2884  ⦋csb 3851

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-sbc 3743  df-csb 3852

This theorem is referenced by:  csbhypf  3879  csbiebt  3880  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  rspc2vd  3899  sbcnestgfw  4375  sbcnestgf  4380  csbnest1g  4386  csbun  4395  csbin  4396  csbdif  4480  csbif  4539  disjors  5083  invdisjrab  5087  disjxiun  5097  disjxun  5098  sbcbr123  5154  eusvnf  5339  reusv2lem4  5348  reusv2  5350  moop2  5458  iunopeqop  5477  pofun  5558  opeliunxp  5699  opeliun2xp  5700  elrnmpt1  5917  resmptf  6006  csbima12  6046  csbcog  6263  fvmpt2f  6950  fvmpts  6953  fvmptdf  6956  fvmpt2i  6960  fvmptex  6964  fmptco  7084  fmptcof  7085  fmptcos  7086  elabrex  7198  elabrexg  7199  fliftfuns  7270  csbov123  7412  ovmpos  7516  fvmpopr2d  7530  ofmpteq  7655  mpomptsx  8018  dmmpossx  8020  fmpox  8021  el2mpocsbcl  8037  offval22  8040  ovmptss  8045  fmpoco  8047  dfmpo  8054  mpoxeldm  8163  mpocurryd  8221  mpocurryvald  8222  fvmpocurryd  8223  eqerlem  8681  qliftfuns  8753  mptelixpg  8885  boxcutc  8891  xpf1o  9079  iunfi  9255  wdom2d  9497  ixpiunwdom  9507  hsmexlem2  10349  ac6c4  10403  iundom2g  10462  seqof2  13995  rlimcld2  15513  nfsum1  15625  sumeq2ii  15628  summolem3  15649  summolem2a  15650  zsum  15653  fsum  15655  sumss2  15661  fsumcvg2  15662  fsumclf  15673  fsumzcl2  15674  fsumsplitf  15677  sumsnf  15678  sumsns  15685  fsummsnunz  15689  fsumsplitsnun  15690  fsum2dlem  15705  fsumcom2  15709  fsumshftm  15716  fsum0diag2  15718  fsum00  15733  fsumabs  15736  fsumrlim  15746  fsumo1  15747  o1fsum  15748  fsumiun  15756  infcvgaux1i  15792  nfcprod1  15843  prodeq2ii  15846  prodmolem3  15868  prodmolem2a  15869  zprod  15872  fprod  15876  fprodntriv  15877  prodss  15882  fprodser  15884  fprodcllemf  15893  prodsn  15897  prodsnf  15899  fprodm1s  15905  fprodp1s  15906  prodsns  15907  fprodabs  15909  fprodn0  15914  fprod2dlem  15915  fprodcom2  15919  fproddivf  15922  fprodsplitf  15923  fprodsplit1f  15925  fprodle  15931  fprodmodd  15932  fprodefsum  16030  sumeven  16326  sumodd  16327  pcmpt  16832  pcmptdvds  16834  natpropd  17915  fucpropd  17916  gsummpt1n0  19906  gsumcom2  19916  gsummptnn0fz  19927  dprd2d2  19987  psrass1lem  21900  mpfrcl  22052  coe1fzgsumdlem  22259  gsummoncoe1  22264  gsumply1eq  22265  evl1gsumdlem  22312  mdetralt2  22565  mdetunilem2  22569  madugsum  22599  fiuncmp  23360  ptcld  23569  ptcldmpt  23570  ptclsg  23571  elmptrab  23783  prdsdsf  24323  prdsxmet  24325  fsumcn  24829  fsum2cn  24830  ovolfiniun  25470  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  ovoliunnul  25476  finiunmbl  25513  volfiniun  25516  iundisj  25517  iundisj2  25518  iunmbl  25522  iunmbl2  25526  itgss3  25784  itgfsum  25796  itgabs  25804  limciun  25863  dvmptfsum  25947  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsumrlim  26006  dvfsumrlim2  26007  dvfsum2  26009  itgsubstlem  26023  itgsubst  26024  rlimcnp2  26944  fsumdvdscom  27163  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  fsumvma  27192  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  iunxpssiun1  32654  disjorsf  32666  disjabrex  32668  disjabrexf  32669  iundisjf  32675  iundisj2f  32676  disjunsn  32680  suppss2f  32727  2ndresdju  32738  fmptdF  32745  fmptcof2  32746  acunirnmpt2f  32750  aciunf1lem  32751  funcnv4mpt  32757  f1od2  32808  iundisjfi  32886  iundisj2fi  32887  fsumiunle  32920  gsummpt2co  33141  gsummptp1  33150  gsumpart  33156  gsumvsca1  33319  gsumvsca2  33320  rmfsupp2  33331  esumpfinvalf  34253  esum2dlem  34269  esumiun  34271  fiunelros  34351  measiun  34395  voliune  34406  volfiniune  34407  sbcaltop  36194  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681  bj-sbeqALT  37145  phpreu  37852  finixpnum  37853  ptrest  37867  poimirlem23  37891  poimirlem24  37892  poimirlem25  37893  poimirlem26  37894  poimirlem27  37895  poimirlem28  37896  mbfposadd  37915  itgabsnc  37937  ftc1cnnclem  37939  ftc2nc  37950  fsumshftd  39325  riotasv2s  39331  cdleme31sn  40753  cdleme31sn1  40754  cdleme31se2  40756  cdleme32fva  40810  cdleme42b  40851  hlhilset  42307  evl1gprodd  42484  idomnnzgmulnz  42500  deg1gprod  42507  fmpocos  42603  mzpsubst  43102  rabdiophlem2  43156  elnn0rabdioph  43157  dvdsrabdioph  43164  fphpd  43170  monotuz  43295  oddcomabszz  43298  wdom2d2  43389  aomclem6  43413  flcidc  43524  fsumcnf  45378  sumsnd  45383  fiiuncl  45422  eliin2f  45460  disjf1  45539  disjrnmpt2  45544  disjinfi  45548  fmptf  45594  fmptff  45624  iuneqfzuzlem  45690  supxrleubrnmptf  45806  fsummulc1f  45928  fsumnncl  45929  fsumf1of  45931  fsumiunss  45932  fsumreclf  45933  fsumlessf  45934  fprodexp  45951  fprodabs2  45952  mccllem  45954  fprodcnlem  45956  fprodcn  45957  climeldmeqmpt  46023  climeldmeqmpt3  46044  climinf2mpt  46069  climinfmpt  46070  limsupequzmptf  46086  fprodcncf  46255  dvmptmulf  46292  dvnmptdivc  46293  dvmptfprod  46300  iblsplitf  46325  fourierdlem86  46547  fourierdlem112  46573  sge0f1o  46737  sge0iunmptlemfi  46768  sge0iunmptlemre  46770  sge0iunmpt  46773  sge0ltfirpmpt2  46781  sge0isummpt2  46787  sge0xaddlem2  46789  sge0xadd  46790  hoimbl2  47020  vonn0ioo2  47045  vonn0icc2  47047  csbafv12g  47494  csbaovg  47537  csbafv212g  47576  fsummsndifre  47729  fsumsplitsndif  47730  fsummmodsndifre  47731  fsummmodsnunz  47732  dmmpossx2  48694