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

This proof depends on syntax axioms:  Ⅎwnfc 2911  ⦋csb 3851

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-sbc 3743  df-csb 3852

This theorem is used by:  csbhypf  3879  csbiebt  3880  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  rspc2vd  3899  sbcnestgfw  4382  sbcnestgf  4387  csbnest1g  4393  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  disjors  5089  invdisjrab  5093  disjxiun  5103  disjxun  5104  sbcbr123  5164  eusvnf  5359  reusv2lem4  5368  reusv2  5370  moop2  5479  iunopeqop  5499  iunopeqopOLD  5500  pofun  5582  opeliunxp  5723  opeliun2xp  5724  elrnmpt1  5950  resmptf  6044  csbima12  6089  csbcog  6321  fvmpt2f  7020  fvmpts  7023  fvmptdf  7026  fvmpt2i  7030  fvmptex  7034  fmptco  7157  fmptcof  7158  fmptcos  7159  elabrex  7272  elabrexg  7273  fliftfuns  7348  csbov123  7490  ovmpos  7595  fvmpopr2d  7609  ofmpteq  7743  mpomptsx  8103  dmmpossx  8105  fmpox  8106  el2mpocsbcl  8124  offval22  8127  ovmptssOLD  8133  fmpoco  8135  f1od2  8138  dfmpo  8143  mpoxeldm  8259  mpocurryd  8317  mpocurryvald  8318  fvmpocurryd  8319  eqerlem  8784  qliftfuns  8856  mptelixpg  8994  boxcutc  9000  xpf1o  9189  iunfi  9363  wdom2d  9604  ixpiunwdom  9614  hsmexlem2  10535  ac6c4  10589  iundom2g  10654  seqof2  14233  rlimcld2  15777  nfsum1  15889  sumeq2ii  15892  summolem3  15912  summolem2a  15913  zsum  15916  fsum  15918  sumss2  15924  fsumcvg2  15925  fsumclf  15936  fsumzcl2  15937  fsumsplitf  15940  sumsnf  15941  sumsns  15948  fsummsnunz  15952  fsumsplitsnun  15953  fsum2dlem  15968  fsumcom2  15972  fsumshftm  15979  fsum0diag2  15981  fsum00  15997  fsumabs  16000  fsumrlim  16010  fsumo1  16011  o1fsum  16012  fsumiun  16020  infcvgaux1i  16058  nfcprod1  16109  prodeq2ii  16112  prodmolem3  16132  prodmolem2a  16133  zprod  16136  fprod  16140  fprodntriv  16141  prodss  16146  fprodser  16148  fprodcllemf  16157  prodsn  16161  prodsnf  16163  fprodm1s  16169  fprodp1s  16170  prodsns  16171  fprodabs  16173  fprodn0  16178  fprod2dlem  16179  fprodcom2  16183  fproddivf  16186  fprodsplitf  16187  fprodsplit1f  16189  fprodle  16195  fprodmodd  16196  fprodefsum  16293  sumeven  16589  sumodd  16590  pcmpt  17102  pcmptdvds  17104  natpropd  18186  fucpropd  18187  gsummpt1n0  20212  gsumcom2  20222  gsummptnn0fz  20233  dprd2d2  20293  psrass1lem  22274  mpfrcl  22427  coe1fzgsumdlem  22654  gsummoncoe1  22659  gsumply1eq  22660  evl1gsumdlem  22707  mdetralt2  22957  mdetunilem2  22961  madugsum  22991  fiuncmp  23755  ptcld  23965  ptcldmpt  23966  ptclsg  23967  elmptrab  24179  prdsdsf  24719  prdsxmet  24721  fsumcn  25224  fsum2cn  25225  ovolfiniun  25855  ovoliunlem3  25858  ovoliun  25859  ovoliun2  25860  ovoliunnul  25861  finiunmbl  25898  volfiniun  25901  iundisj  25902  iundisj2  25903  iunmbl  25907  iunmbl2  25911  itgss3  26168  itgfsum  26180  itgabs  26188  limciun  26247  dvmptfsum  26328  dvfsumle  26374  dvfsumabs  26376  dvfsumlem1  26379  dvfsumlem2  26380  dvfsumlem3  26381  dvfsumlem4  26382  dvfsumrlim  26384  dvfsumrlim2  26385  dvfsum2  26387  itgsubstlem  26401  itgsubst  26402  rlimcnp2  27327  fsumdvdscom  27545  fsumdvdsmul  27555  fsumvma  27573  dchrisumlema  27848  dchrisumlem2  27850  dchrisumlem3  27851  iunxpssiun1  33237  disjorsf  33249  disjabrex  33251  disjabrexf  33252  iundisjf  33258  iundisj2f  33259  disjunsn  33263  suppss2f  33307  2ndresdju  33318  fmptdf2  33325  fmptcof2  33326  acunirnmpt2f  33330  aciunf1lem  33331  funcnv4mpt  33337  iundisjfi  33461  iundisj2fi  33462  fsumiunle  33493  gsummpt2co  33685  gsummptp1  33694  gsumpart  33700  gsumvsca1  33863  gsumvsca2  33864  rmfsupp2  33874  esumpfinvalf  34791  esum2dlem  34807  esumiun  34809  fiunelros  34890  measiun  34934  voliune  34945  volfiniune  34946  sbcaltop  36937  weiunpo  37444  weiunso  37445  weiunfr  37446  weiunse  37447  csbttc  37488  bj-sbeqALT  38003  phpreu  38732  finixpnum  38733  ptrest  38742  poimirlem23  38766  poimirlem24  38767  poimirlem25  38768  poimirlem26  38769  poimirlem27  38770  poimirlem28  38771  mbfposadd  38790  itgabsnc  38812  ftc1cnnclem  38814  ftc2nc  38825  fsumshftd  40212  riotasv2s  40218  cdleme31sn  41640  cdleme31sn1  41641  cdleme31se2  41643  cdleme32fva  41697  cdleme42b  41738  hlhilset  43194  evl1gprodd  43370  idomnnzgmulnz  43386  deg1gprod  43393  fmpocos  43491  mzpsubst  43963  rabdiophlem2  44013  elnn0rabdioph  44014  dvdsrabdioph  44021  fphpd  44027  monotuz  44152  oddcomabszz  44155  wdom2d2  44246  aomclem6  44265  flcidc  44375  fsumcnf  46254  sumsnd  46259  fiiuncl  46298  eliin2f  46334  disjf1  46413  disjrnmpt2  46418  disjinfi  46422  fmptf  46466  fmptff  46496  iuneqfzuzlem  46561  supxrleubrnmptf  46676  fsummulc1f  46798  fsumnncl  46799  fsumf1of  46801  fsumiunss  46802  fsumreclf  46803  fsumlessf  46804  fprodexp  46821  fprodabs2  46822  mccllem  46824  fprodcnlem  46826  fprodcn  46827  climeldmeqmpt  46893  climeldmeqmpt3  46914  climinf2mpt  46939  climinfmpt  46940  limsupequzmptf  46956  fprodcncf  47125  dvmptmulf  47162  dvnmptdivc  47163  dvmptfprod  47170  iblsplitf  47195  fourierdlem86  47417  fourierdlem112  47443  sge0f1o  47607  sge0iunmptlemfi  47638  sge0iunmptlemre  47640  sge0iunmpt  47643  sge0ltfirpmpt2  47651  sge0isummpt2  47657  sge0xaddlem2  47659  sge0xadd  47660  hoimbl2  47890  vonn0ioo2  47915  vonn0icc2  47917  csbafv12g  48422  csbaovg  48465  csbafv212g  48504  fsummsndifre  48665  fsumsplitsndif  48666  fsummmodsndifre  48667  fsummmodsnunz  48668  dmmpossx2  49664