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  4073  invdisjrab  4076  disjiun  4077  sbcbrg  4137  moop2  4337  pofun  4402  eusvnf  4543  opeliunxp  4773  elrnmpt1  4974  resmptf  5054  csbima12g  5088  fvmpts  5711  fvmpt2  5717  mptfvex  5719  fmptco  5800  fmptcof  5801  fmptcos  5802  elabrex  5880  elabrexg  5881  fliftfuns  5921  csbov123g  6039  ovmpos  6127  fvmpopr2d  6140  mpomptsx  6341  dmmpossx  6343  fmpox  6344  mpofvex  6349  fmpoco  6360  dfmpo  6367  f1od2  6379  disjxp1  6380  eqerlem  6709  qliftfuns  6764  mptelixpg  6879  xpf1o  7001  iunfidisj  7109  cc3  7450  seq3f1olemstep  10731  seq3f1olemp  10732  nfsum1  11862  sumeq2  11865  sumfct  11880  sumrbdclem  11883  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsumgcl  11892  fsum3  11893  isumss  11897  isumss2  11899  fsum3cvg2  11900  fsumzcl2  11911  fsumsplitf  11914  sumsnf  11915  sumsns  11921  fsumsplitsnun  11925  fsum2dlemstep  11940  fisumcom2  11944  fsumshftm  11951  fisum0diag2  11953  fsummulc2  11954  fsum00  11968  fsumabs  11971  fsumrelem  11977  fsumiun  11983  isumshft  11996  mertenslem2  12042  nfcprod1  12060  prodeq2  12063  prodrbdclem  12077  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodntrivap  12090  prodfct  12093  prodssdc  12095  fprodmul  12097  prodsnf  12098  fprodm1s  12107  fprodp1s  12108  prodsns  12109  fprodcl2lem  12111  fprodcllemf  12119  fprodabs  12122  fprodap0  12127  fprod2dlemstep  12128  fprodcom2fi  12132  fprodrec  12135  fproddivapf  12137  fprodsplitf  12138  fprodsplit1f  12140  fprodap0f  12142  fprodle  12146  fprodmodd  12147  pcmpt  12861  pcmptdvds  12863  ctiunctlemudc  13003  ctiunctlemf  13004  ctiunct  13006  ctiunctal  13007  gsumfzfsumlemm  14545  iuncld  14783  fsumcncntop  15235  limcmpted  15331  dvmptfsum  15393  fsumdvdsmul  15659