Theorem nfcsb1v 3907

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

Syntax hints:  Ⅎwnfc 2961  ⦋csb 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sbc 3773  df-csb 3884

This theorem is referenced by:  csbhypf  3911  csbiebt  3912  cbvrabcsfw  3924  cbvralcsf  3925  cbvreucsf  3927  cbvrabcsf  3928  rspc2vd  3932  sbcnestgfw  4370  sbcnestgf  4375  csbnest1g  4381  csbun  4390  csbin  4391  csbif  4522  disjors  5040  invdisjrabw  5044  invdisjrab  5045  disjxiun  5056  disjxun  5057  sbcbr123  5113  eusvnf  5285  reusv2lem4  5294  reusv2  5296  moop2  5385  iunopeqop  5404  pofun  5486  opeliunxp  5614  elrnmpt1  5825  resmptf  5902  csbima12  5942  fvmpt2f  6764  fvmpts  6766  fvmptdf  6769  fvmpt2i  6773  fvmptex  6777  fmptco  6886  fmptcof  6887  fmptcos  6888  elabrex  6996  fliftfuns  7061  csbov123  7192  ovmpos  7292  ofmpteq  7422  mpomptsx  7756  dmmpossx  7758  fmpox  7759  el2mpocsbcl  7774  offval22  7777  ovmptss  7782  fmpoco  7784  dfmpo  7791  mpoxeldm  7871  mpocurryd  7929  mpocurryvald  7930  fvmpocurryd  7931  eqerlem  8317  qliftfuns  8378  mptelixpg  8493  boxcutc  8499  xpf1o  8673  iunfi  8806  wdom2d  9038  ixpiunwdom  9049  hsmexlem2  9843  ac6c4  9897  iundom2g  9956  seqof2  13422  rlimcld2  14929  nfsum1  15040  sumeq2ii  15044  summolem3  15065  summolem2a  15066  zsum  15069  fsum  15071  sumss2  15077  fsumcvg2  15078  fsumzcl2  15089  fsumsplitf  15092  sumsnf  15093  sumsns  15099  fsummsnunz  15103  fsumsplitsnun  15104  fsum2dlem  15119  fsumcom2  15123  fsumshftm  15130  fsum0diag2  15132  fsum00  15147  fsumabs  15150  fsumrlim  15160  fsumo1  15161  o1fsum  15162  fsumiun  15170  infcvgaux1i  15206  nfcprod1  15258  prodeq2ii  15261  prodmolem3  15281  prodmolem2a  15282  zprod  15285  fprod  15289  fprodntriv  15290  prodss  15295  fprodser  15297  fprodcllemf  15306  prodsn  15310  prodsnf  15312  fprodm1s  15318  fprodp1s  15319  prodsns  15320  fprodabs  15322  fprodn0  15327  fprod2dlem  15328  fprodcom2  15332  fproddivf  15335  fprodsplitf  15336  fprodsplit1f  15338  fprodle  15344  fprodmodd  15345  fprodefsum  15442  sumeven  15732  sumodd  15733  pcmpt  16222  pcmptdvds  16224  natpropd  17240  fucpropd  17241  gsummpt1n0  19079  gsumcom2  19089  gsummptnn0fz  19100  dprd2d2  19160  psrass1lem  20151  mpfrcl  20292  coe1fzgsumdlem  20463  gsummoncoe1  20466  gsumply1eq  20467  evl1gsumdlem  20513  mdetralt2  21212  mdetunilem2  21216  madugsum  21246  fiuncmp  22006  ptcld  22215  ptcldmpt  22216  ptclsg  22217  elmptrab  22429  prdsdsf  22971  prdsxmet  22973  fsumcn  23472  fsum2cn  23473  ovolfiniun  24096  ovoliunlem3  24099  ovoliun  24100  ovoliun2  24101  ovoliunnul  24102  finiunmbl  24139  volfiniun  24142  iundisj  24143  iundisj2  24144  iunmbl  24148  iunmbl2  24152  itgss3  24409  itgfsum  24421  itgabs  24429  limciun  24486  dvmptfsum  24566  dvfsumle  24612  dvfsumabs  24614  dvfsumlem1  24617  dvfsumlem2  24618  dvfsumlem3  24619  dvfsumlem4  24620  dvfsumrlim  24622  dvfsumrlim2  24623  dvfsum2  24625  itgsubstlem  24639  itgsubst  24640  rlimcnp2  25538  fsumdvdscom  25756  fsumdvdsmul  25766  fsumvma  25783  dchrisumlema  26058  dchrisumlem2  26060  dchrisumlem3  26061  disjorsf  30324  disjabrex  30326  disjabrexf  30327  iundisjf  30333  iundisj2f  30334  disjunsn  30338  suppss2f  30378  fmptdF  30395  fmptcof2  30396  acunirnmpt2f  30400  aciunf1lem  30401  funcnv4mpt  30408  f1od2  30451  iundisjfi  30513  iundisj2fi  30514  fsumiunle  30540  gsummpt2co  30681  gsumvsca1  30849  gsumvsca2  30850  rmfsupp2  30861  esumpfinvalf  31330  esum2dlem  31346  esumiun  31348  fiunelros  31428  measiun  31472  voliune  31483  volfiniune  31484  sbcaltop  33437  bj-sbeqALT  34212  csbdif  34600  phpreu  34870  finixpnum  34871  ptrest  34885  poimirlem23  34909  poimirlem24  34910  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  mbfposadd  34933  itgabsnc  34955  ftc1cnnclem  34959  ftc2nc  34970  fsumshftd  36082  riotasv2s  36088  cdleme31sn  37510  cdleme31sn1  37511  cdleme31se2  37513  cdleme32fva  37567  cdleme42b  37608  hlhilset  39064  mzpsubst  39338  rabdiophlem2  39392  elnn0rabdioph  39393  dvdsrabdioph  39400  fphpd  39406  monotuz  39531  oddcomabszz  39534  wdom2d2  39625  aomclem6  39652  flcidc  39767  csbcog  39987  fsumcnf  41271  sumsnd  41276  elabrexg  41296  fiiuncl  41320  eliin2f  41363  disjf1  41435  disjrnmpt2  41441  disjinfi  41446  fmptf  41501  iuneqfzuzlem  41594  supxrleubrnmptf  41719  fsumclf  41842  fsummulc1f  41843  fsumnncl  41844  fsumf1of  41847  fsumiunss  41848  fsumreclf  41849  fsumlessf  41850  fprodexp  41867  fprodabs2  41868  mccllem  41870  fprodcnlem  41872  fprodcn  41873  climeldmeqmpt  41941  climeldmeqmpt3  41962  climinf2mpt  41987  climinfmpt  41988  limsupequzmptf  42004  fprodcncf  42176  dvmptmulf  42214  dvnmptdivc  42215  dvmptfprod  42222  iblsplitf  42247  fourierdlem86  42470  fourierdlem112  42496  sge0iunmptlemfi  42688  sge0iunmptlemre  42690  sge0iunmpt  42693  sge0ltfirpmpt2  42701  sge0isummpt2  42707  sge0xaddlem2  42709  sge0xadd  42710  hoimbl2  42940  vonn0ioo2  42965  vonn0icc2  42967  csbafv12g  43329  csbaovg  43372  csbafv212g  43411  fsummsndifre  43525  fsumsplitsndif  43526  fsummmodsndifre  43527  fsummmodsnunz  43528  opeliun2xp  44374  dmmpossx2  44378