Theorem nfcsb1v 3126

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

Syntax hints:   F/_wnfc 2335   [_csb 3093

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-sbc 2999  df-csb 3094

This theorem is referenced by:  csbhypf  3132  csbiebt  3133  sbcnestgf  3145  csbnest1g  3149  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  rspc2vd  3162  csbing  3380  disjnims  4036  disjiun  4039  sbcbrg  4098  moop2  4296  pofun  4359  eusvnf  4500  opeliunxp  4730  elrnmpt1  4929  resmptf  5009  csbima12g  5043  fvmpts  5657  fvmpt2  5663  mptfvex  5665  fmptco  5746  fmptcof  5747  fmptcos  5748  elabrex  5826  elabrexg  5827  fliftfuns  5867  csbov123g  5983  ovmpos  6069  fvmpopr2d  6082  mpomptsx  6283  dmmpossx  6285  fmpox  6286  mpofvex  6291  fmpoco  6302  dfmpo  6309  f1od2  6321  disjxp1  6322  eqerlem  6651  qliftfuns  6706  mptelixpg  6821  xpf1o  6941  iunfidisj  7048  cc3  7380  seq3f1olemstep  10659  seq3f1olemp  10660  nfsum1  11667  sumeq2  11670  sumfct  11685  sumrbdclem  11688  summodclem3  11691  summodclem2a  11692  zsumdc  11695  fsumgcl  11697  fsum3  11698  isumss  11702  isumss2  11704  fsum3cvg2  11705  fsumzcl2  11716  fsumsplitf  11719  sumsnf  11720  sumsns  11726  fsumsplitsnun  11730  fsum2dlemstep  11745  fisumcom2  11749  fsumshftm  11756  fisum0diag2  11758  fsummulc2  11759  fsum00  11773  fsumabs  11776  fsumrelem  11782  fsumiun  11788  isumshft  11801  mertenslem2  11847  nfcprod1  11865  prodeq2  11868  prodrbdclem  11882  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodntrivap  11895  prodfct  11898  prodssdc  11900  fprodmul  11902  prodsnf  11903  fprodm1s  11912  fprodp1s  11913  prodsns  11914  fprodcl2lem  11916  fprodcllemf  11924  fprodabs  11927  fprodap0  11932  fprod2dlemstep  11933  fprodcom2fi  11937  fprodrec  11940  fproddivapf  11942  fprodsplitf  11943  fprodsplit1f  11945  fprodap0f  11947  fprodle  11951  fprodmodd  11952  pcmpt  12666  pcmptdvds  12668  ctiunctlemudc  12808  ctiunctlemf  12809  ctiunct  12811  ctiunctal  12812  gsumfzfsumlemm  14349  iuncld  14587  fsumcncntop  15039  limcmpted  15135  dvmptfsum  15197  fsumdvdsmul  15463