Theorem nfcsb1v 3174

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

Syntax hints:  Ⅎwnfc 2373  ⦋csb 3141

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 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-sbc 3046  df-csb 3142

This theorem is referenced by:  csbhypf  3180  csbiebt  3181  sbcnestgf  3193  csbnest1g  3197  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  rspc2vd  3210  csbing  3432  disjnims  4105  invdisjrab  4108  disjiun  4109  sbcbrg  4169  moop2  4373  pofun  4438  eusvnf  4579  opeliunxp  4810  elrnmpt1  5013  resmptf  5093  csbima12g  5128  fvmpts  5760  fvmpt2  5766  mptfvex  5768  fmptco  5848  fmptcof  5849  fmptcos  5850  elabrex  5936  elabrexg  5937  fliftfuns  5977  csbov123g  6097  ovmpos  6185  fvmpopr2d  6198  mpomptsx  6406  dmmpossx  6408  fmpox  6409  mpofvex  6414  fmpoco  6425  dfmpo  6432  f1od2  6444  disjxp1  6445  eqerlem  6811  qliftfuns  6866  mptelixpg  6982  xpf1o  7110  iunfidisj  7226  cc3  7598  seq3f1olemstep  10903  seq3f1olemp  10904  nfsum1  12070  sumeq2  12073  sumfct  12088  sumrbdclem  12092  summodclem3  12095  summodclem2a  12096  zsumdc  12099  fsumgcl  12101  fsum3  12102  isumss  12106  isumss2  12108  fsum3cvg2  12109  fsumzcl2  12120  fsumsplitf  12123  sumsnf  12124  sumsns  12130  fsumsplitsnun  12134  fsum2dlemstep  12149  fisumcom2  12153  fsumshftm  12160  fisum0diag2  12162  fsummulc2  12163  fsum00  12177  fsumabs  12180  fsumrelem  12186  fsumiun  12192  isumshft  12205  mertenslem2  12251  nfcprod1  12269  prodeq2  12272  prodrbdclem  12286  prodmodclem3  12290  prodmodclem2a  12291  zproddc  12294  fprodseq  12298  fprodntrivap  12299  prodfct  12302  prodssdc  12304  fprodmul  12306  prodsnf  12307  fprodm1s  12316  fprodp1s  12317  prodsns  12318  fprodcl2lem  12320  fprodcllemf  12328  fprodabs  12331  fprodap0  12336  fprod2dlemstep  12337  fprodcom2fi  12341  fprodrec  12344  fproddivapf  12346  fprodsplitf  12347  fprodsplit1f  12349  fprodap0f  12351  fprodle  12355  fprodmodd  12356  pcmpt  13070  pcmptdvds  13072  ctiunctlemudc  13276  ctiunctlemf  13277  ctiunct  13279  ctiunctal  13280  gsumfzfsumlemm  14865  iuncld  15110  fsumcncntop  15562  limcmpted  15658  dvmptfsum  15720  fsumdvdsmul  15989