Theorem nfcsb1v 3125

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

Syntax hints:   F/_wnfc 2334   [_csb 3092

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-sbc 2998  df-csb 3093

This theorem is referenced by:  csbhypf  3131  csbiebt  3132  sbcnestgf  3144  csbnest1g  3148  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  rspc2vd  3161  csbing  3379  disjnims  4035  disjiun  4038  sbcbrg  4097  moop2  4295  pofun  4358  eusvnf  4499  opeliunxp  4729  elrnmpt1  4928  resmptf  5008  csbima12g  5042  fvmpts  5656  fvmpt2  5662  mptfvex  5664  fmptco  5745  fmptcof  5746  fmptcos  5747  elabrex  5825  elabrexg  5826  fliftfuns  5866  csbov123g  5982  ovmpos  6068  fvmpopr2d  6081  mpomptsx  6282  dmmpossx  6284  fmpox  6285  mpofvex  6290  fmpoco  6301  dfmpo  6308  f1od2  6320  disjxp1  6321  eqerlem  6650  qliftfuns  6705  mptelixpg  6820  xpf1o  6940  iunfidisj  7047  cc3  7379  seq3f1olemstep  10657  seq3f1olemp  10658  nfsum1  11638  sumeq2  11641  sumfct  11656  sumrbdclem  11659  summodclem3  11662  summodclem2a  11663  zsumdc  11666  fsumgcl  11668  fsum3  11669  isumss  11673  isumss2  11675  fsum3cvg2  11676  fsumzcl2  11687  fsumsplitf  11690  sumsnf  11691  sumsns  11697  fsumsplitsnun  11701  fsum2dlemstep  11716  fisumcom2  11720  fsumshftm  11727  fisum0diag2  11729  fsummulc2  11730  fsum00  11744  fsumabs  11747  fsumrelem  11753  fsumiun  11759  isumshft  11772  mertenslem2  11818  nfcprod1  11836  prodeq2  11839  prodrbdclem  11853  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodntrivap  11866  prodfct  11869  prodssdc  11871  fprodmul  11873  prodsnf  11874  fprodm1s  11883  fprodp1s  11884  prodsns  11885  fprodcl2lem  11887  fprodcllemf  11895  fprodabs  11898  fprodap0  11903  fprod2dlemstep  11904  fprodcom2fi  11908  fprodrec  11911  fproddivapf  11913  fprodsplitf  11914  fprodsplit1f  11916  fprodap0f  11918  fprodle  11922  fprodmodd  11923  pcmpt  12637  pcmptdvds  12639  ctiunctlemudc  12779  ctiunctlemf  12780  ctiunct  12782  ctiunctal  12783  gsumfzfsumlemm  14320  iuncld  14558  fsumcncntop  15010  limcmpted  15106  dvmptfsum  15168  fsumdvdsmul  15434