Theorem nfcsb1v 3158

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 3157	1 |- F/_ x [_ A / x ]_ B

Syntax hints:   F/_wnfc 2359   [_csb 3125

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 3030  df-csb 3126

This theorem is referenced by:  csbhypf  3164  csbiebt  3165  sbcnestgf  3177  csbnest1g  3181  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  rspc2vd  3194  csbing  3412  disjnims  4077  invdisjrab  4080  disjiun  4081  sbcbrg  4141  moop2  4342  pofun  4407  eusvnf  4548  opeliunxp  4779  elrnmpt1  4981  resmptf  5061  csbima12g  5095  fvmpts  5720  fvmpt2  5726  mptfvex  5728  fmptco  5809  fmptcof  5810  fmptcos  5811  elabrex  5893  elabrexg  5894  fliftfuns  5934  csbov123g  6052  ovmpos  6140  fvmpopr2d  6153  mpomptsx  6357  dmmpossx  6359  fmpox  6360  mpofvex  6365  fmpoco  6376  dfmpo  6383  f1od2  6395  disjxp1  6396  eqerlem  6728  qliftfuns  6783  mptelixpg  6898  xpf1o  7025  iunfidisj  7136  cc3  7477  seq3f1olemstep  10766  seq3f1olemp  10767  nfsum1  11907  sumeq2  11910  sumfct  11925  sumrbdclem  11928  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsumgcl  11937  fsum3  11938  isumss  11942  isumss2  11944  fsum3cvg2  11945  fsumzcl2  11956  fsumsplitf  11959  sumsnf  11960  sumsns  11966  fsumsplitsnun  11970  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fisum0diag2  11998  fsummulc2  11999  fsum00  12013  fsumabs  12016  fsumrelem  12022  fsumiun  12028  isumshft  12041  mertenslem2  12087  nfcprod1  12105  prodeq2  12108  prodrbdclem  12122  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodntrivap  12135  prodfct  12138  prodssdc  12140  fprodmul  12142  prodsnf  12143  fprodm1s  12152  fprodp1s  12153  prodsns  12154  fprodcl2lem  12156  fprodcllemf  12164  fprodabs  12167  fprodap0  12172  fprod2dlemstep  12173  fprodcom2fi  12177  fprodrec  12180  fproddivapf  12182  fprodsplitf  12183  fprodsplit1f  12185  fprodap0f  12187  fprodle  12191  fprodmodd  12192  pcmpt  12906  pcmptdvds  12908  ctiunctlemudc  13048  ctiunctlemf  13049  ctiunct  13051  ctiunctal  13052  gsumfzfsumlemm  14591  iuncld  14829  fsumcncntop  15281  limcmpted  15377  dvmptfsum  15439  fsumdvdsmul  15705