Theorem nfcsb1v 3128

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	⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfcsb1v

Step	Hyp	Ref	Expression
1		nfcv 2349	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfcsb1 3127	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  Ⅎwnfc 2336  ⦋csb 3095

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 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-sbc 3001  df-csb 3096

This theorem is referenced by:  csbhypf  3134  csbiebt  3135  sbcnestgf  3147  csbnest1g  3151  cbvralcsf  3158  cbvrexcsf  3159  cbvreucsf  3160  cbvrabcsf  3161  rspc2vd  3164  csbing  3382  disjnims  4039  invdisjrab  4042  disjiun  4043  sbcbrg  4103  moop2  4301  pofun  4364  eusvnf  4505  opeliunxp  4735  elrnmpt1  4935  resmptf  5015  csbima12g  5049  fvmpts  5667  fvmpt2  5673  mptfvex  5675  fmptco  5756  fmptcof  5757  fmptcos  5758  elabrex  5836  elabrexg  5837  fliftfuns  5877  csbov123g  5993  ovmpos  6079  fvmpopr2d  6092  mpomptsx  6293  dmmpossx  6295  fmpox  6296  mpofvex  6301  fmpoco  6312  dfmpo  6319  f1od2  6331  disjxp1  6332  eqerlem  6661  qliftfuns  6716  mptelixpg  6831  xpf1o  6953  iunfidisj  7060  cc3  7393  seq3f1olemstep  10672  seq3f1olemp  10673  nfsum1  11717  sumeq2  11720  sumfct  11735  sumrbdclem  11738  summodclem3  11741  summodclem2a  11742  zsumdc  11745  fsumgcl  11747  fsum3  11748  isumss  11752  isumss2  11754  fsum3cvg2  11755  fsumzcl2  11766  fsumsplitf  11769  sumsnf  11770  sumsns  11776  fsumsplitsnun  11780  fsum2dlemstep  11795  fisumcom2  11799  fsumshftm  11806  fisum0diag2  11808  fsummulc2  11809  fsum00  11823  fsumabs  11826  fsumrelem  11832  fsumiun  11838  isumshft  11851  mertenslem2  11897  nfcprod1  11915  prodeq2  11918  prodrbdclem  11932  prodmodclem3  11936  prodmodclem2a  11937  zproddc  11940  fprodseq  11944  fprodntrivap  11945  prodfct  11948  prodssdc  11950  fprodmul  11952  prodsnf  11953  fprodm1s  11962  fprodp1s  11963  prodsns  11964  fprodcl2lem  11966  fprodcllemf  11974  fprodabs  11977  fprodap0  11982  fprod2dlemstep  11983  fprodcom2fi  11987  fprodrec  11990  fproddivapf  11992  fprodsplitf  11993  fprodsplit1f  11995  fprodap0f  11997  fprodle  12001  fprodmodd  12002  pcmpt  12716  pcmptdvds  12718  ctiunctlemudc  12858  ctiunctlemf  12859  ctiunct  12861  ctiunctal  12862  gsumfzfsumlemm  14399  iuncld  14637  fsumcncntop  15089  limcmpted  15185  dvmptfsum  15247  fsumdvdsmul  15513