Theorem nfcsb1v 3874

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

This proof depends on syntax axioms:  Ⅎwnfc 2909  ⦋csb 3850

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 2215  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-sbc 3743  df-csb 3851

This theorem is used by:  csbhypf  3878  csbiebt  3879  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  rspc2vd  3898  sbcnestgfw  4382  sbcnestgf  4387  csbnest1g  4393  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  disjors  5090  invdisjrab  5094  disjxiun  5104  disjxun  5105  sbcbr123  5163  eusvnf  5361  reusv2lem4  5370  reusv2  5372  moop2  5483  iunopeqop  5502  iunopeqopOLD  5503  pofun  5585  opeliunxp  5726  opeliun2xp  5727  elrnmpt1  5948  resmptf  6039  csbima12  6079  csbcog  6299  fvmpt2f  6991  fvmpts  6994  fvmptdf  6997  fvmpt2i  7001  fvmptex  7005  fmptco  7127  fmptcof  7128  fmptcos  7129  elabrex  7243  elabrexg  7244  fliftfuns  7319  csbov123  7461  ovmpos  7565  fvmpopr2d  7579  ofmpteq  7705  mpomptsx  8065  dmmpossx  8067  fmpox  8068  el2mpocsbcl  8086  offval22  8089  ovmptss  8094  fmpoco  8096  dfmpo  8103  mpoxeldm  8213  mpocurryd  8271  mpocurryvald  8272  fvmpocurryd  8273  eqerlem  8736  qliftfuns  8808  mptelixpg  8946  boxcutc  8952  xpf1o  9141  iunfi  9314  wdom2d  9556  ixpiunwdom  9566  hsmexlem2  10433  ac6c4  10487  iundom2g  10552  seqof2  14128  rlimcld2  15669  nfsum1  15781  sumeq2ii  15784  summolem3  15804  summolem2a  15805  zsum  15808  fsum  15810  sumss2  15816  fsumcvg2  15817  fsumclf  15828  fsumzcl2  15829  fsumsplitf  15832  sumsnf  15833  sumsns  15840  fsummsnunz  15844  fsumsplitsnun  15845  fsum2dlem  15860  fsumcom2  15864  fsumshftm  15871  fsum0diag2  15873  fsum00  15889  fsumabs  15892  fsumrlim  15902  fsumo1  15903  o1fsum  15904  fsumiun  15912  infcvgaux1i  15950  nfcprod1  16001  prodeq2ii  16004  prodmolem3  16026  prodmolem2a  16027  zprod  16030  fprod  16034  fprodntriv  16035  prodss  16040  fprodser  16042  fprodcllemf  16051  prodsn  16055  prodsnf  16057  fprodm1s  16063  fprodp1s  16064  prodsns  16065  fprodabs  16067  fprodn0  16072  fprod2dlem  16073  fprodcom2  16077  fproddivf  16080  fprodsplitf  16081  fprodsplit1f  16083  fprodle  16089  fprodmodd  16090  fprodefsum  16187  sumeven  16483  sumodd  16484  pcmpt  16990  pcmptdvds  16992  natpropd  18074  fucpropd  18075  gsummpt1n0  20098  gsumcom2  20108  gsummptnn0fz  20119  dprd2d2  20179  psrass1lem  22154  mpfrcl  22307  coe1fzgsumdlem  22534  gsummoncoe1  22539  gsumply1eq  22540  evl1gsumdlem  22587  mdetralt2  22837  mdetunilem2  22841  madugsum  22871  fiuncmp  23635  ptcld  23845  ptcldmpt  23846  ptclsg  23847  elmptrab  24059  prdsdsf  24599  prdsxmet  24601  fsumcn  25104  fsum2cn  25105  ovolfiniun  25735  ovoliunlem3  25738  ovoliun  25739  ovoliun2  25740  ovoliunnul  25741  finiunmbl  25778  volfiniun  25781  iundisj  25782  iundisj2  25783  iunmbl  25787  iunmbl2  25791  itgss3  26049  itgfsum  26061  itgabs  26069  limciun  26128  dvmptfsum  26209  dvfsumle  26255  dvfsumabs  26257  dvfsumlem1  26260  dvfsumlem2  26261  dvfsumlem3  26262  dvfsumlem4  26263  dvfsumrlim  26265  dvfsumrlim2  26266  dvfsum2  26268  itgsubstlem  26282  itgsubst  26283  rlimcnp2  27211  fsumdvdscom  27429  fsumdvdsmul  27439  fsumvma  27457  dchrisumlema  27732  dchrisumlem2  27734  dchrisumlem3  27735  iunxpssiun1  33049  disjorsf  33061  disjabrex  33063  disjabrexf  33064  iundisjf  33070  iundisj2f  33071  disjunsn  33075  suppss2f  33119  2ndresdju  33130  fmptdf2  33137  fmptcof2  33138  acunirnmpt2f  33142  aciunf1lem  33143  funcnv4mpt  33149  f1od2  33198  iundisjfi  33275  iundisj2fi  33276  fsumiunle  33307  gsummpt2co  33496  gsummptp1  33505  gsumpart  33511  gsumvsca1  33674  gsumvsca2  33675  rmfsupp2  33685  esumpfinvalf  34594  esum2dlem  34610  esumiun  34612  fiunelros  34693  measiun  34737  voliune  34748  volfiniune  34749  sbcaltop  36569  weiunpo  37092  weiunso  37093  weiunfr  37094  weiunse  37095  csbttc  37136  bj-sbeqALT  37651  phpreu  38366  finixpnum  38367  ptrest  38376  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  mbfposadd  38424  itgabsnc  38446  ftc1cnnclem  38448  ftc2nc  38459  fsumshftd  39833  riotasv2s  39839  cdleme31sn  41261  cdleme31sn1  41262  cdleme31se2  41264  cdleme32fva  41318  cdleme42b  41359  hlhilset  42815  evl1gprodd  42991  idomnnzgmulnz  43007  deg1gprod  43014  fmpocos  43111  mzpsubst  43601  rabdiophlem2  43651  elnn0rabdioph  43652  dvdsrabdioph  43659  fphpd  43665  monotuz  43790  oddcomabszz  43793  wdom2d2  43884  aomclem6  43908  flcidc  44019  fsumcnf  45863  sumsnd  45868  fiiuncl  45907  eliin2f  45944  disjf1  46023  disjrnmpt2  46028  disjinfi  46032  fmptf  46076  fmptff  46106  iuneqfzuzlem  46172  supxrleubrnmptf  46287  fsummulc1f  46409  fsumnncl  46410  fsumf1of  46412  fsumiunss  46413  fsumreclf  46414  fsumlessf  46415  fprodexp  46432  fprodabs2  46433  mccllem  46435  fprodcnlem  46437  fprodcn  46438  climeldmeqmpt  46504  climeldmeqmpt3  46525  climinf2mpt  46550  climinfmpt  46551  limsupequzmptf  46567  fprodcncf  46736  dvmptmulf  46773  dvnmptdivc  46774  dvmptfprod  46781  iblsplitf  46806  fourierdlem86  47028  fourierdlem112  47054  sge0f1o  47218  sge0iunmptlemfi  47249  sge0iunmptlemre  47251  sge0iunmpt  47254  sge0ltfirpmpt2  47262  sge0isummpt2  47268  sge0xaddlem2  47270  sge0xadd  47271  hoimbl2  47501  vonn0ioo2  47526  vonn0icc2  47528  csbafv12g  48033  csbaovg  48076  csbafv212g  48115  fsummsndifre  48276  fsumsplitsndif  48277  fsummmodsndifre  48278  fsummmodsnunz  48279  dmmpossx2  49275