Theorem nfcsb1v 3160

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 2374	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfcsb1 3159	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  Ⅎwnfc 2361  ⦋csb 3127

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-sbc 3032  df-csb 3128

This theorem is referenced by:  csbhypf  3166  csbiebt  3167  sbcnestgf  3179  csbnest1g  3183  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rspc2vd  3196  csbing  3414  disjnims  4079  invdisjrab  4082  disjiun  4083  sbcbrg  4143  moop2  4344  pofun  4409  eusvnf  4550  opeliunxp  4781  elrnmpt1  4983  resmptf  5063  csbima12g  5097  fvmpts  5724  fvmpt2  5730  mptfvex  5732  fmptco  5813  fmptcof  5814  fmptcos  5815  elabrex  5898  elabrexg  5899  fliftfuns  5939  csbov123g  6057  ovmpos  6145  fvmpopr2d  6158  mpomptsx  6362  dmmpossx  6364  fmpox  6365  mpofvex  6370  fmpoco  6381  dfmpo  6388  f1od2  6400  disjxp1  6401  eqerlem  6733  qliftfuns  6788  mptelixpg  6903  xpf1o  7030  iunfidisj  7145  cc3  7487  seq3f1olemstep  10777  seq3f1olemp  10778  nfsum1  11921  sumeq2  11924  sumfct  11939  sumrbdclem  11943  summodclem3  11946  summodclem2a  11947  zsumdc  11950  fsumgcl  11952  fsum3  11953  isumss  11957  isumss2  11959  fsum3cvg2  11960  fsumzcl2  11971  fsumsplitf  11974  sumsnf  11975  sumsns  11981  fsumsplitsnun  11985  fsum2dlemstep  12000  fisumcom2  12004  fsumshftm  12011  fisum0diag2  12013  fsummulc2  12014  fsum00  12028  fsumabs  12031  fsumrelem  12037  fsumiun  12043  isumshft  12056  mertenslem2  12102  nfcprod1  12120  prodeq2  12123  prodrbdclem  12137  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  fprodntrivap  12150  prodfct  12153  prodssdc  12155  fprodmul  12157  prodsnf  12158  fprodm1s  12167  fprodp1s  12168  prodsns  12169  fprodcl2lem  12171  fprodcllemf  12179  fprodabs  12182  fprodap0  12187  fprod2dlemstep  12188  fprodcom2fi  12192  fprodrec  12195  fproddivapf  12197  fprodsplitf  12198  fprodsplit1f  12200  fprodap0f  12202  fprodle  12206  fprodmodd  12207  pcmpt  12921  pcmptdvds  12923  ctiunctlemudc  13063  ctiunctlemf  13064  ctiunct  13066  ctiunctal  13067  gsumfzfsumlemm  14607  iuncld  14845  fsumcncntop  15297  limcmpted  15393  dvmptfsum  15455  fsumdvdsmul  15721