Theorem nfcsb1v 3160

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

Syntax hints:   F/_wnfc 2361   [_csb 3127

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-sbc 3032  df-csb 3128

This theorem is referenced by:  csbhypf  3166  csbiebt  3167  sbcnestgf  3179  csbnest1g  3183  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rspc2vd  3196  csbing  3414  disjnims  4079  invdisjrab  4082  disjiun  4083  sbcbrg  4143  moop2  4344  pofun  4409  eusvnf  4550  opeliunxp  4781  elrnmpt1  4983  resmptf  5063  csbima12g  5097  fvmpts  5724  fvmpt2  5730  mptfvex  5732  fmptco  5813  fmptcof  5814  fmptcos  5815  elabrex  5897  elabrexg  5898  fliftfuns  5938  csbov123g  6056  ovmpos  6144  fvmpopr2d  6157  mpomptsx  6361  dmmpossx  6363  fmpox  6364  mpofvex  6369  fmpoco  6380  dfmpo  6387  f1od2  6399  disjxp1  6400  eqerlem  6732  qliftfuns  6787  mptelixpg  6902  xpf1o  7029  iunfidisj  7144  cc3  7486  seq3f1olemstep  10775  seq3f1olemp  10776  nfsum1  11916  sumeq2  11919  sumfct  11934  sumrbdclem  11937  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsumgcl  11946  fsum3  11947  isumss  11951  isumss2  11953  fsum3cvg2  11954  fsumzcl2  11965  fsumsplitf  11968  sumsnf  11969  sumsns  11975  fsumsplitsnun  11979  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fisum0diag2  12007  fsummulc2  12008  fsum00  12022  fsumabs  12025  fsumrelem  12031  fsumiun  12037  isumshft  12050  mertenslem2  12096  nfcprod1  12114  prodeq2  12117  prodrbdclem  12131  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prodfct  12147  prodssdc  12149  fprodmul  12151  prodsnf  12152  fprodm1s  12161  fprodp1s  12162  prodsns  12163  fprodcl2lem  12165  fprodcllemf  12173  fprodabs  12176  fprodap0  12181  fprod2dlemstep  12182  fprodcom2fi  12186  fprodrec  12189  fproddivapf  12191  fprodsplitf  12192  fprodsplit1f  12194  fprodap0f  12196  fprodle  12200  fprodmodd  12201  pcmpt  12915  pcmptdvds  12917  ctiunctlemudc  13057  ctiunctlemf  13058  ctiunct  13060  ctiunctal  13061  gsumfzfsumlemm  14600  iuncld  14838  fsumcncntop  15290  limcmpted  15386  dvmptfsum  15448  fsumdvdsmul  15714