Theorem nfcsb1v 3174

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

Syntax hints:  Ⅎwnfc 2373  ⦋csb 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-sbc 3046  df-csb 3142

This theorem is referenced by:  csbhypf  3180  csbiebt  3181  sbcnestgf  3193  csbnest1g  3197  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  rspc2vd  3210  csbing  3432  disjnims  4105  invdisjrab  4108  disjiun  4109  sbcbrg  4169  moop2  4373  pofun  4438  eusvnf  4579  opeliunxp  4810  elrnmpt1  5013  resmptf  5093  csbima12g  5128  fvmpts  5760  fvmpt2  5766  mptfvex  5768  fmptco  5848  fmptcof  5849  fmptcos  5850  elabrex  5936  elabrexg  5937  fliftfuns  5977  csbov123g  6097  ovmpos  6185  fvmpopr2d  6198  mpomptsx  6406  dmmpossx  6408  fmpox  6409  mpofvex  6414  fmpoco  6425  dfmpo  6432  f1od2  6444  disjxp1  6445  eqerlem  6811  qliftfuns  6866  mptelixpg  6982  xpf1o  7110  iunfidisj  7226  cc3  7598  seq3f1olemstep  10900  seq3f1olemp  10901  nfsum1  12066  sumeq2  12069  sumfct  12084  sumrbdclem  12088  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsumgcl  12097  fsum3  12098  isumss  12102  isumss2  12104  fsum3cvg2  12105  fsumzcl2  12116  fsumsplitf  12119  sumsnf  12120  sumsns  12126  fsumsplitsnun  12130  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fisum0diag2  12158  fsummulc2  12159  fsum00  12173  fsumabs  12176  fsumrelem  12182  fsumiun  12188  isumshft  12201  mertenslem2  12247  nfcprod1  12265  prodeq2  12268  prodrbdclem  12282  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prodfct  12298  prodssdc  12300  fprodmul  12302  prodsnf  12303  fprodm1s  12312  fprodp1s  12313  prodsns  12314  fprodcl2lem  12316  fprodcllemf  12324  fprodabs  12327  fprodap0  12332  fprod2dlemstep  12333  fprodcom2fi  12337  fprodrec  12340  fproddivapf  12342  fprodsplitf  12343  fprodsplit1f  12345  fprodap0f  12347  fprodle  12351  fprodmodd  12352  pcmpt  13066  pcmptdvds  13068  ctiunctlemudc  13272  ctiunctlemf  13273  ctiunct  13275  ctiunctal  13276  gsumfzfsumlemm  14847  iuncld  15092  fsumcncntop  15544  limcmpted  15640  dvmptfsum  15702  fsumdvdsmul  15971