Theorem nfcsb1v 3082

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	|- F/_ x [_ A / x ]_ B

Distinct variable group:   x, A

Allowed substitution hint:   B( x)

Proof of Theorem nfcsb1v

Step	Hyp	Ref	Expression
1		nfcv 2312	. 2 |- F/_ x A
2	1	nfcsb1 3081	1 |- F/_ x [_ A / x ]_ B

Syntax hints:   F/_wnfc 2299   [_csb 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-sbc 2956  df-csb 3050

This theorem is referenced by:  csbhypf  3087  csbiebt  3088  sbcnestgf  3100  csbnest1g  3104  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  rspc2vd  3117  csbing  3334  disjnims  3981  disjiun  3984  sbcbrg  4043  moop2  4236  pofun  4297  eusvnf  4438  opeliunxp  4666  elrnmpt1  4862  resmptf  4941  csbima12g  4972  fvmpts  5574  fvmpt2  5579  mptfvex  5581  fmptco  5662  fmptcof  5663  fmptcos  5664  elabrex  5737  fliftfuns  5777  csbov123g  5891  ovmpos  5976  mpomptsx  6176  dmmpossx  6178  fmpox  6179  mpofvex  6182  fmpoco  6195  dfmpo  6202  f1od2  6214  disjxp1  6215  eqerlem  6544  qliftfuns  6597  mptelixpg  6712  xpf1o  6822  iunfidisj  6923  cc3  7230  seq3f1olemstep  10457  seq3f1olemp  10458  nfsum1  11319  sumeq2  11322  sumfct  11337  sumrbdclem  11340  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumgcl  11349  fsum3  11350  isumss  11354  isumss2  11356  fsum3cvg2  11357  fsumzcl2  11368  fsumsplitf  11371  sumsnf  11372  sumsns  11378  fsumsplitsnun  11382  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  fsummulc2  11411  fsum00  11425  fsumabs  11428  fsumrelem  11434  fsumiun  11440  isumshft  11453  mertenslem2  11499  nfcprod1  11517  prodeq2  11520  prodrbdclem  11534  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prodfct  11550  prodssdc  11552  fprodmul  11554  prodsnf  11555  fprodm1s  11564  fprodp1s  11565  prodsns  11566  fprodcl2lem  11568  fprodcllemf  11576  fprodabs  11579  fprodap0  11584  fprod2dlemstep  11585  fprodcom2fi  11589  fprodrec  11592  fproddivapf  11594  fprodsplitf  11595  fprodsplit1f  11597  fprodap0f  11599  fprodle  11603  fprodmodd  11604  pcmpt  12295  pcmptdvds  12297  ctiunctlemudc  12392  ctiunctlemf  12393  ctiunct  12395  ctiunctal  12396  iuncld  12909  fsumcncntop  13350  limcmpted  13426