Theorem nfcsb1v 3161

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

Syntax hints:   F/_wnfc 2362   [_csb 3128

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-sbc 3033  df-csb 3129

This theorem is referenced by:  csbhypf  3167  csbiebt  3168  sbcnestgf  3180  csbnest1g  3184  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  rspc2vd  3197  csbing  3416  disjnims  4084  invdisjrab  4087  disjiun  4088  sbcbrg  4148  moop2  4350  pofun  4415  eusvnf  4556  opeliunxp  4787  elrnmpt1  4989  resmptf  5069  csbima12g  5104  fvmpts  5733  fvmpt2  5739  mptfvex  5741  fmptco  5821  fmptcof  5822  fmptcos  5823  elabrex  5908  elabrexg  5909  fliftfuns  5949  csbov123g  6067  ovmpos  6155  fvmpopr2d  6168  mpomptsx  6371  dmmpossx  6373  fmpox  6374  mpofvex  6379  fmpoco  6390  dfmpo  6397  f1od2  6409  disjxp1  6410  eqerlem  6776  qliftfuns  6831  mptelixpg  6946  xpf1o  7073  iunfidisj  7188  cc3  7530  seq3f1olemstep  10822  seq3f1olemp  10823  nfsum1  11979  sumeq2  11982  sumfct  11997  sumrbdclem  12001  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsumgcl  12010  fsum3  12011  isumss  12015  isumss2  12017  fsum3cvg2  12018  fsumzcl2  12029  fsumsplitf  12032  sumsnf  12033  sumsns  12039  fsumsplitsnun  12043  fsum2dlemstep  12058  fisumcom2  12062  fsumshftm  12069  fisum0diag2  12071  fsummulc2  12072  fsum00  12086  fsumabs  12089  fsumrelem  12095  fsumiun  12101  isumshft  12114  mertenslem2  12160  nfcprod1  12178  prodeq2  12181  prodrbdclem  12195  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodntrivap  12208  prodfct  12211  prodssdc  12213  fprodmul  12215  prodsnf  12216  fprodm1s  12225  fprodp1s  12226  prodsns  12227  fprodcl2lem  12229  fprodcllemf  12237  fprodabs  12240  fprodap0  12245  fprod2dlemstep  12246  fprodcom2fi  12250  fprodrec  12253  fproddivapf  12255  fprodsplitf  12256  fprodsplit1f  12258  fprodap0f  12260  fprodle  12264  fprodmodd  12265  pcmpt  12979  pcmptdvds  12981  ctiunctlemudc  13121  ctiunctlemf  13122  ctiunct  13124  ctiunctal  13125  gsumfzfsumlemm  14666  iuncld  14909  fsumcncntop  15361  limcmpted  15457  dvmptfsum  15519  fsumdvdsmul  15788