Theorem nfcsb1v 3092

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

Syntax hints:   F/_wnfc 2306   [_csb 3059

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-sbc 2965  df-csb 3060

This theorem is referenced by:  csbhypf  3097  csbiebt  3098  sbcnestgf  3110  csbnest1g  3114  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  rspc2vd  3127  csbing  3344  disjnims  3997  disjiun  4000  sbcbrg  4059  moop2  4253  pofun  4314  eusvnf  4455  opeliunxp  4683  elrnmpt1  4880  resmptf  4959  csbima12g  4991  fvmpts  5596  fvmpt2  5601  mptfvex  5603  fmptco  5684  fmptcof  5685  fmptcos  5686  elabrex  5760  elabrexg  5761  fliftfuns  5801  csbov123g  5915  ovmpos  6000  mpomptsx  6200  dmmpossx  6202  fmpox  6203  mpofvex  6206  fmpoco  6219  dfmpo  6226  f1od2  6238  disjxp1  6239  eqerlem  6568  qliftfuns  6621  mptelixpg  6736  xpf1o  6846  iunfidisj  6947  cc3  7269  seq3f1olemstep  10503  seq3f1olemp  10504  nfsum1  11366  sumeq2  11369  sumfct  11384  sumrbdclem  11387  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsumgcl  11396  fsum3  11397  isumss  11401  isumss2  11403  fsum3cvg2  11404  fsumzcl2  11415  fsumsplitf  11418  sumsnf  11419  sumsns  11425  fsumsplitsnun  11429  fsum2dlemstep  11444  fisumcom2  11448  fsumshftm  11455  fisum0diag2  11457  fsummulc2  11458  fsum00  11472  fsumabs  11475  fsumrelem  11481  fsumiun  11487  isumshft  11500  mertenslem2  11546  nfcprod1  11564  prodeq2  11567  prodrbdclem  11581  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodntrivap  11594  prodfct  11597  prodssdc  11599  fprodmul  11601  prodsnf  11602  fprodm1s  11611  fprodp1s  11612  prodsns  11613  fprodcl2lem  11615  fprodcllemf  11623  fprodabs  11626  fprodap0  11631  fprod2dlemstep  11632  fprodcom2fi  11636  fprodrec  11639  fproddivapf  11641  fprodsplitf  11642  fprodsplit1f  11644  fprodap0f  11646  fprodle  11650  fprodmodd  11651  pcmpt  12343  pcmptdvds  12345  ctiunctlemudc  12440  ctiunctlemf  12441  ctiunct  12443  ctiunctal  12444  iuncld  13700  fsumcncntop  14141  limcmpted  14217