Theorem nfcsb1v 3170

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

Syntax hints:  Ⅎwnfc 2371  ⦋csb 3137

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-sbc 3042  df-csb 3138

This theorem is referenced by:  csbhypf  3176  csbiebt  3177  sbcnestgf  3189  csbnest1g  3193  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  rspc2vd  3206  csbing  3427  disjnims  4099  invdisjrab  4102  disjiun  4103  sbcbrg  4163  moop2  4367  pofun  4432  eusvnf  4573  opeliunxp  4804  elrnmpt1  5007  resmptf  5087  csbima12g  5122  fvmpts  5754  fvmpt2  5760  mptfvex  5762  fmptco  5842  fmptcof  5843  fmptcos  5844  elabrex  5929  elabrexg  5930  fliftfuns  5970  csbov123g  6088  ovmpos  6176  fvmpopr2d  6189  mpomptsx  6392  dmmpossx  6394  fmpox  6395  mpofvex  6400  fmpoco  6411  dfmpo  6418  f1od2  6430  disjxp1  6431  eqerlem  6797  qliftfuns  6852  mptelixpg  6968  xpf1o  7096  iunfidisj  7212  cc3  7581  seq3f1olemstep  10875  seq3f1olemp  10876  nfsum1  12037  sumeq2  12040  sumfct  12055  sumrbdclem  12059  summodclem3  12062  summodclem2a  12063  zsumdc  12066  fsumgcl  12068  fsum3  12069  isumss  12073  isumss2  12075  fsum3cvg2  12076  fsumzcl2  12087  fsumsplitf  12090  sumsnf  12091  sumsns  12097  fsumsplitsnun  12101  fsum2dlemstep  12116  fisumcom2  12120  fsumshftm  12127  fisum0diag2  12129  fsummulc2  12130  fsum00  12144  fsumabs  12147  fsumrelem  12153  fsumiun  12159  isumshft  12172  mertenslem2  12218  nfcprod1  12236  prodeq2  12239  prodrbdclem  12253  prodmodclem3  12257  prodmodclem2a  12258  zproddc  12261  fprodseq  12265  fprodntrivap  12266  prodfct  12269  prodssdc  12271  fprodmul  12273  prodsnf  12274  fprodm1s  12283  fprodp1s  12284  prodsns  12285  fprodcl2lem  12287  fprodcllemf  12295  fprodabs  12298  fprodap0  12303  fprod2dlemstep  12304  fprodcom2fi  12308  fprodrec  12311  fproddivapf  12313  fprodsplitf  12314  fprodsplit1f  12316  fprodap0f  12318  fprodle  12322  fprodmodd  12323  pcmpt  13037  pcmptdvds  13039  ctiunctlemudc  13180  ctiunctlemf  13181  ctiunct  13183  ctiunctal  13184  gsumfzfsumlemm  14727  iuncld  14972  fsumcncntop  15424  limcmpted  15520  dvmptfsum  15582  fsumdvdsmul  15851