Theorem nfcsb1v 3157

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

Syntax hints:   F/_wnfc 2359   [_csb 3124

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-sbc 3029  df-csb 3125

This theorem is referenced by:  csbhypf  3163  csbiebt  3164  sbcnestgf  3176  csbnest1g  3180  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  rspc2vd  3193  csbing  3411  disjnims  4074  invdisjrab  4077  disjiun  4078  sbcbrg  4138  moop2  4338  pofun  4403  eusvnf  4544  opeliunxp  4774  elrnmpt1  4975  resmptf  5055  csbima12g  5089  fvmpts  5714  fvmpt2  5720  mptfvex  5722  fmptco  5803  fmptcof  5804  fmptcos  5805  elabrex  5887  elabrexg  5888  fliftfuns  5928  csbov123g  6046  ovmpos  6134  fvmpopr2d  6147  mpomptsx  6349  dmmpossx  6351  fmpox  6352  mpofvex  6357  fmpoco  6368  dfmpo  6375  f1od2  6387  disjxp1  6388  eqerlem  6719  qliftfuns  6774  mptelixpg  6889  xpf1o  7013  iunfidisj  7124  cc3  7465  seq3f1olemstep  10748  seq3f1olemp  10749  nfsum1  11882  sumeq2  11885  sumfct  11900  sumrbdclem  11903  summodclem3  11906  summodclem2a  11907  zsumdc  11910  fsumgcl  11912  fsum3  11913  isumss  11917  isumss2  11919  fsum3cvg2  11920  fsumzcl2  11931  fsumsplitf  11934  sumsnf  11935  sumsns  11941  fsumsplitsnun  11945  fsum2dlemstep  11960  fisumcom2  11964  fsumshftm  11971  fisum0diag2  11973  fsummulc2  11974  fsum00  11988  fsumabs  11991  fsumrelem  11997  fsumiun  12003  isumshft  12016  mertenslem2  12062  nfcprod1  12080  prodeq2  12083  prodrbdclem  12097  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prodfct  12113  prodssdc  12115  fprodmul  12117  prodsnf  12118  fprodm1s  12127  fprodp1s  12128  prodsns  12129  fprodcl2lem  12131  fprodcllemf  12139  fprodabs  12142  fprodap0  12147  fprod2dlemstep  12148  fprodcom2fi  12152  fprodrec  12155  fproddivapf  12157  fprodsplitf  12158  fprodsplit1f  12160  fprodap0f  12162  fprodle  12166  fprodmodd  12167  pcmpt  12881  pcmptdvds  12883  ctiunctlemudc  13023  ctiunctlemf  13024  ctiunct  13026  ctiunctal  13027  gsumfzfsumlemm  14566  iuncld  14804  fsumcncntop  15256  limcmpted  15352  dvmptfsum  15414  fsumdvdsmul  15680