Theorem nfcsb1v 3134

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

Syntax hints:   F/_wnfc 2337   [_csb 3101

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-sbc 3006  df-csb 3102

This theorem is referenced by:  csbhypf  3140  csbiebt  3141  sbcnestgf  3153  csbnest1g  3157  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  rspc2vd  3170  csbing  3388  disjnims  4050  invdisjrab  4053  disjiun  4054  sbcbrg  4114  moop2  4314  pofun  4377  eusvnf  4518  opeliunxp  4748  elrnmpt1  4948  resmptf  5028  csbima12g  5062  fvmpts  5680  fvmpt2  5686  mptfvex  5688  fmptco  5769  fmptcof  5770  fmptcos  5771  elabrex  5849  elabrexg  5850  fliftfuns  5890  csbov123g  6006  ovmpos  6092  fvmpopr2d  6105  mpomptsx  6306  dmmpossx  6308  fmpox  6309  mpofvex  6314  fmpoco  6325  dfmpo  6332  f1od2  6344  disjxp1  6345  eqerlem  6674  qliftfuns  6729  mptelixpg  6844  xpf1o  6966  iunfidisj  7074  cc3  7415  seq3f1olemstep  10696  seq3f1olemp  10697  nfsum1  11782  sumeq2  11785  sumfct  11800  sumrbdclem  11803  summodclem3  11806  summodclem2a  11807  zsumdc  11810  fsumgcl  11812  fsum3  11813  isumss  11817  isumss2  11819  fsum3cvg2  11820  fsumzcl2  11831  fsumsplitf  11834  sumsnf  11835  sumsns  11841  fsumsplitsnun  11845  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fisum0diag2  11873  fsummulc2  11874  fsum00  11888  fsumabs  11891  fsumrelem  11897  fsumiun  11903  isumshft  11916  mertenslem2  11962  nfcprod1  11980  prodeq2  11983  prodrbdclem  11997  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodntrivap  12010  prodfct  12013  prodssdc  12015  fprodmul  12017  prodsnf  12018  fprodm1s  12027  fprodp1s  12028  prodsns  12029  fprodcl2lem  12031  fprodcllemf  12039  fprodabs  12042  fprodap0  12047  fprod2dlemstep  12048  fprodcom2fi  12052  fprodrec  12055  fproddivapf  12057  fprodsplitf  12058  fprodsplit1f  12060  fprodap0f  12062  fprodle  12066  fprodmodd  12067  pcmpt  12781  pcmptdvds  12783  ctiunctlemudc  12923  ctiunctlemf  12924  ctiunct  12926  ctiunctal  12927  gsumfzfsumlemm  14464  iuncld  14702  fsumcncntop  15154  limcmpted  15250  dvmptfsum  15312  fsumdvdsmul  15578