Theorem nfcsb1v 3105

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

Syntax hints:  Ⅎwnfc 2319  ⦋csb 3072

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-sbc 2978  df-csb 3073

This theorem is referenced by:  csbhypf  3110  csbiebt  3111  sbcnestgf  3123  csbnest1g  3127  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  rspc2vd  3140  csbing  3357  disjnims  4010  disjiun  4013  sbcbrg  4072  moop2  4266  pofun  4327  eusvnf  4468  opeliunxp  4696  elrnmpt1  4893  resmptf  4972  csbima12g  5004  fvmpts  5610  fvmpt2  5615  mptfvex  5617  fmptco  5698  fmptcof  5699  fmptcos  5700  elabrex  5774  elabrexg  5775  fliftfuns  5815  csbov123g  5929  ovmpos  6015  mpomptsx  6216  dmmpossx  6218  fmpox  6219  mpofvex  6222  fmpoco  6235  dfmpo  6242  f1od2  6254  disjxp1  6255  eqerlem  6584  qliftfuns  6637  mptelixpg  6752  xpf1o  6862  iunfidisj  6963  cc3  7285  seq3f1olemstep  10519  seq3f1olemp  10520  nfsum1  11382  sumeq2  11385  sumfct  11400  sumrbdclem  11403  summodclem3  11406  summodclem2a  11407  zsumdc  11410  fsumgcl  11412  fsum3  11413  isumss  11417  isumss2  11419  fsum3cvg2  11420  fsumzcl2  11431  fsumsplitf  11434  sumsnf  11435  sumsns  11441  fsumsplitsnun  11445  fsum2dlemstep  11460  fisumcom2  11464  fsumshftm  11471  fisum0diag2  11473  fsummulc2  11474  fsum00  11488  fsumabs  11491  fsumrelem  11497  fsumiun  11503  isumshft  11516  mertenslem2  11562  nfcprod1  11580  prodeq2  11583  prodrbdclem  11597  prodmodclem3  11601  prodmodclem2a  11602  zproddc  11605  fprodseq  11609  fprodntrivap  11610  prodfct  11613  prodssdc  11615  fprodmul  11617  prodsnf  11618  fprodm1s  11627  fprodp1s  11628  prodsns  11629  fprodcl2lem  11631  fprodcllemf  11639  fprodabs  11642  fprodap0  11647  fprod2dlemstep  11648  fprodcom2fi  11652  fprodrec  11655  fproddivapf  11657  fprodsplitf  11658  fprodsplit1f  11660  fprodap0f  11662  fprodle  11666  fprodmodd  11667  pcmpt  12359  pcmptdvds  12361  ctiunctlemudc  12456  ctiunctlemf  12457  ctiunct  12459  ctiunctal  12460  iuncld  14012  fsumcncntop  14453  limcmpted  14529