Theorem nfcsb1v 3871

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

This proof depends on syntax axioms:  Ⅎwnfc 2908  ⦋csb 3847

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-sbc 3740  df-csb 3848

This theorem is used by:  csbhypf  3875  csbiebt  3876  cbvrabcsfw  3888  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  rspc2vd  3895  sbcnestgfw  4379  sbcnestgf  4384  csbnest1g  4390  csbun  4399  csbin  4400  csbdif  4481  csbif  4540  disjors  5086  invdisjrab  5090  disjxiun  5100  disjxun  5101  sbcbr123  5159  eusvnf  5354  reusv2lem4  5363  reusv2  5365  moop2  5474  iunopeqop  5494  iunopeqopOLD  5495  pofun  5577  opeliunxp  5718  opeliun2xp  5719  elrnmpt1  5942  resmptf  6033  csbima12  6073  csbcog  6293  fvmpt2f  6986  fvmpts  6989  fvmptdf  6992  fvmpt2i  6996  fvmptex  7000  fmptco  7122  fmptcof  7123  fmptcos  7124  elabrex  7238  elabrexg  7239  fliftfuns  7314  csbov123  7456  ovmpos  7560  fvmpopr2d  7574  ofmpteq  7705  mpomptsx  8064  dmmpossx  8066  fmpox  8067  el2mpocsbcl  8085  offval22  8088  ovmptss  8093  fmpoco  8095  dfmpo  8102  mpoxeldm  8212  mpocurryd  8270  mpocurryvald  8271  fvmpocurryd  8272  eqerlem  8737  qliftfuns  8809  mptelixpg  8947  boxcutc  8953  xpf1o  9142  iunfi  9316  wdom2d  9558  ixpiunwdom  9568  hsmexlem2  10486  ac6c4  10540  iundom2g  10605  seqof2  14183  rlimcld2  15725  nfsum1  15837  sumeq2ii  15840  summolem3  15860  summolem2a  15861  zsum  15864  fsum  15866  sumss2  15872  fsumcvg2  15873  fsumclf  15884  fsumzcl2  15885  fsumsplitf  15888  sumsnf  15889  sumsns  15896  fsummsnunz  15900  fsumsplitsnun  15901  fsum2dlem  15916  fsumcom2  15920  fsumshftm  15927  fsum0diag2  15929  fsum00  15945  fsumabs  15948  fsumrlim  15958  fsumo1  15959  o1fsum  15960  fsumiun  15968  infcvgaux1i  16006  nfcprod1  16057  prodeq2ii  16060  prodmolem3  16080  prodmolem2a  16081  zprod  16084  fprod  16088  fprodntriv  16089  prodss  16094  fprodser  16096  fprodcllemf  16105  prodsn  16109  prodsnf  16111  fprodm1s  16117  fprodp1s  16118  prodsns  16119  fprodabs  16121  fprodn0  16126  fprod2dlem  16127  fprodcom2  16131  fproddivf  16134  fprodsplitf  16135  fprodsplit1f  16137  fprodle  16143  fprodmodd  16144  fprodefsum  16241  sumeven  16537  sumodd  16538  pcmpt  17050  pcmptdvds  17052  natpropd  18134  fucpropd  18135  gsummpt1n0  20159  gsumcom2  20169  gsummptnn0fz  20180  dprd2d2  20240  psrass1lem  22221  mpfrcl  22374  coe1fzgsumdlem  22601  gsummoncoe1  22606  gsumply1eq  22607  evl1gsumdlem  22654  mdetralt2  22904  mdetunilem2  22908  madugsum  22938  fiuncmp  23702  ptcld  23912  ptcldmpt  23913  ptclsg  23914  elmptrab  24126  prdsdsf  24666  prdsxmet  24668  fsumcn  25171  fsum2cn  25172  ovolfiniun  25802  ovoliunlem3  25805  ovoliun  25806  ovoliun2  25807  ovoliunnul  25808  finiunmbl  25845  volfiniun  25848  iundisj  25849  iundisj2  25850  iunmbl  25854  iunmbl2  25858  itgss3  26115  itgfsum  26127  itgabs  26135  limciun  26194  dvmptfsum  26275  dvfsumle  26321  dvfsumabs  26323  dvfsumlem1  26326  dvfsumlem2  26327  dvfsumlem3  26328  dvfsumlem4  26329  dvfsumrlim  26331  dvfsumrlim2  26332  dvfsum2  26334  itgsubstlem  26348  itgsubst  26349  rlimcnp2  27276  fsumdvdscom  27494  fsumdvdsmul  27504  fsumvma  27522  dchrisumlema  27797  dchrisumlem2  27799  dchrisumlem3  27800  iunxpssiun1  33144  disjorsf  33156  disjabrex  33158  disjabrexf  33159  iundisjf  33165  iundisj2f  33166  disjunsn  33170  suppss2f  33214  2ndresdju  33225  fmptdf2  33232  fmptcof2  33233  acunirnmpt2f  33237  aciunf1lem  33238  funcnv4mpt  33244  f1od2  33293  iundisjfi  33370  iundisj2fi  33371  fsumiunle  33402  gsummpt2co  33591  gsummptp1  33600  gsumpart  33606  gsumvsca1  33769  gsumvsca2  33770  rmfsupp2  33780  esumpfinvalf  34690  esum2dlem  34706  esumiun  34708  fiunelros  34789  measiun  34833  voliune  34844  volfiniune  34845  sbcaltop  36716  weiunpo  37223  weiunso  37224  weiunfr  37225  weiunse  37226  csbttc  37267  bj-sbeqALT  37782  phpreu  38495  finixpnum  38496  ptrest  38505  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem26  38532  poimirlem27  38533  poimirlem28  38534  mbfposadd  38553  itgabsnc  38575  ftc1cnnclem  38577  ftc2nc  38588  fsumshftd  39977  riotasv2s  39983  cdleme31sn  41405  cdleme31sn1  41406  cdleme31se2  41408  cdleme32fva  41462  cdleme42b  41503  hlhilset  42959  evl1gprodd  43135  idomnnzgmulnz  43151  deg1gprod  43158  fmpocos  43255  mzpsubst  43712  rabdiophlem2  43762  elnn0rabdioph  43763  dvdsrabdioph  43770  fphpd  43776  monotuz  43901  oddcomabszz  43904  wdom2d2  43995  aomclem6  44019  flcidc  44130  fsumcnf  45981  sumsnd  45986  fiiuncl  46025  eliin2f  46062  disjf1  46141  disjrnmpt2  46146  disjinfi  46150  fmptf  46194  fmptff  46224  iuneqfzuzlem  46290  supxrleubrnmptf  46405  fsummulc1f  46527  fsumnncl  46528  fsumf1of  46530  fsumiunss  46531  fsumreclf  46532  fsumlessf  46533  fprodexp  46550  fprodabs2  46551  mccllem  46553  fprodcnlem  46555  fprodcn  46556  climeldmeqmpt  46622  climeldmeqmpt3  46643  climinf2mpt  46668  climinfmpt  46669  limsupequzmptf  46685  fprodcncf  46854  dvmptmulf  46891  dvnmptdivc  46892  dvmptfprod  46899  iblsplitf  46924  fourierdlem86  47146  fourierdlem112  47172  sge0f1o  47336  sge0iunmptlemfi  47367  sge0iunmptlemre  47369  sge0iunmpt  47372  sge0ltfirpmpt2  47380  sge0isummpt2  47386  sge0xaddlem2  47388  sge0xadd  47389  hoimbl2  47619  vonn0ioo2  47644  vonn0icc2  47646  csbafv12g  48151  csbaovg  48194  csbafv212g  48233  fsummsndifre  48394  fsumsplitsndif  48395  fsummmodsndifre  48396  fsummmodsnunz  48397  dmmpossx2  49393