Theorem nfcsb1v 3060

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 2296	. 2 |- F/_ x A
2	1	nfcsb1 3059	1 |- F/_ x [_ A / x ]_ B

Syntax hints:   F/_wnfc 2283   [_csb 3027

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-sbc 2934  df-csb 3028

This theorem is referenced by:  csbhypf  3065  csbiebt  3066  sbcnestgf  3078  csbnest1g  3082  cbvralcsf  3089  cbvrexcsf  3090  cbvreucsf  3091  cbvrabcsf  3092  csbing  3310  disjnims  3953  disjiun  3956  sbcbrg  4014  moop2  4206  pofun  4267  eusvnf  4407  opeliunxp  4634  elrnmpt1  4830  resmptf  4909  csbima12g  4940  fvmpts  5539  fvmpt2  5544  mptfvex  5546  fmptco  5626  fmptcof  5627  fmptcos  5628  elabrex  5699  fliftfuns  5739  csbov123g  5849  ovmpos  5934  mpomptsx  6135  dmmpossx  6137  fmpox  6138  mpofvex  6141  fmpoco  6153  dfmpo  6160  f1od2  6172  disjxp1  6173  eqerlem  6500  qliftfuns  6553  mptelixpg  6668  xpf1o  6778  iunfidisj  6879  cc3  7167  seq3f1olemstep  10378  seq3f1olemp  10379  nfsum1  11230  sumeq2  11233  sumfct  11248  sumrbdclem  11251  summodclem3  11254  summodclem2a  11255  zsumdc  11258  fsumgcl  11260  fsum3  11261  isumss  11265  isumss2  11267  fsum3cvg2  11268  fsumzcl2  11279  fsumsplitf  11282  sumsnf  11283  sumsns  11289  fsumsplitsnun  11293  fsum2dlemstep  11308  fisumcom2  11312  fsumshftm  11319  fisum0diag2  11321  fsummulc2  11322  fsum00  11336  fsumabs  11339  fsumrelem  11345  fsumiun  11351  isumshft  11364  mertenslem2  11410  nfcprod1  11428  prodeq2  11431  prodrbdclem  11445  prodmodclem3  11449  prodmodclem2a  11450  zproddc  11453  fprodseq  11457  fprodntrivap  11458  prodfct  11461  prodssdc  11463  fprodmul  11465  prodsnf  11466  fprodm1s  11475  fprodp1s  11476  prodsns  11477  fprodcl2lem  11479  fprodcllemf  11487  fprodabs  11490  fprodap0  11495  fprod2dlemstep  11496  fprodcom2fi  11500  fprodrec  11503  fproddivapf  11505  fprodsplitf  11506  fprodsplit1f  11508  fprodap0f  11510  fprodle  11514  fprodmodd  11515  ctiunctlemudc  12125  ctiunctlemf  12126  ctiunct  12128  ctiunctal  12129  iuncld  12462  fsumcncntop  12903  limcmpted  12979