Theorem nfcsb1v 3180

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

Syntax hints:   F/_wnfc 2379   [_csb 3147

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-sbc 3052  df-csb 3148

This theorem is referenced by:  csbhypf  3186  csbiebt  3187  sbcnestgf  3199  csbnest1g  3203  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rspc2vd  3216  csbing  3438  disjnims  4116  invdisjrab  4119  disjiun  4120  sbcbrg  4180  moop2  4387  pofun  4452  eusvnf  4594  opeliunxp  4825  elrnmpt1  5028  resmptf  5108  csbima12g  5143  fvmpts  5777  fvmpt2  5783  mptfvex  5785  fmptco  5865  fmptcof  5866  fmptcos  5867  elabrex  5953  elabrexg  5954  fliftfuns  5994  csbov123g  6114  ovmpos  6202  fvmpopr2d  6215  mpomptsx  6423  dmmpossx  6425  fmpox  6426  mpofvex  6431  fmpoco  6442  dfmpo  6449  f1od2  6461  disjxp1  6462  eqerlem  6828  qliftfuns  6883  mptelixpg  7006  xpf1o  7134  iunfidisj  7250  cc3  7624  seq3f1olemstep  10929  seq3f1olemp  10930  nfsum1  12100  sumeq2  12103  sumfct  12118  sumrbdclem  12122  summodclem3  12125  summodclem2a  12126  zsumdc  12129  fsumgcl  12131  fsum3  12132  isumss  12136  isumss2  12138  fsum3cvg2  12139  fsumzcl2  12150  fsumsplitf  12153  sumsnf  12154  sumsns  12160  fsumsplitsnun  12164  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fisum0diag2  12192  fsummulc2  12193  fsum00  12207  fsumabs  12210  fsumrelem  12216  fsumiun  12222  isumshft  12235  mertenslem2  12281  nfcprod1  12299  prodeq2  12302  prodrbdclem  12316  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodntrivap  12329  prodfct  12332  prodssdc  12334  fprodmul  12336  prodsnf  12337  fprodm1s  12346  fprodp1s  12347  prodsns  12348  fprodcl2lem  12350  fprodcllemf  12358  fprodabs  12361  fprodap0  12366  fprod2dlemstep  12367  fprodcom2fi  12371  fprodrec  12374  fproddivapf  12376  fprodsplitf  12377  fprodsplit1f  12379  fprodap0f  12381  fprodle  12385  fprodmodd  12386  pcmpt  13100  pcmptdvds  13102  ctiunctlemudc  13306  ctiunctlemf  13307  ctiunct  13309  ctiunctal  13310  gsummptfidmadd  14138  gsumfsum  14895  iuncld  15139  fsumcncntop  15591  limcmpted  15687  dvmptfsum  15749  fsumdvdsmul  16019