Theorem nfcsb1v 3157

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

Syntax hints:  Ⅎwnfc 2359  ⦋csb 3124

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-sbc 3029  df-csb 3125

This theorem is referenced by:  csbhypf  3163  csbiebt  3164  sbcnestgf  3176  csbnest1g  3180  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  rspc2vd  3193  csbing  3411  disjnims  4073  invdisjrab  4076  disjiun  4077  sbcbrg  4137  moop2  4337  pofun  4400  eusvnf  4541  opeliunxp  4771  elrnmpt1  4971  resmptf  5051  csbima12g  5085  fvmpts  5705  fvmpt2  5711  mptfvex  5713  fmptco  5794  fmptcof  5795  fmptcos  5796  elabrex  5874  elabrexg  5875  fliftfuns  5915  csbov123g  6033  ovmpos  6119  fvmpopr2d  6132  mpomptsx  6333  dmmpossx  6335  fmpox  6336  mpofvex  6341  fmpoco  6352  dfmpo  6359  f1od2  6371  disjxp1  6372  eqerlem  6701  qliftfuns  6756  mptelixpg  6871  xpf1o  6993  iunfidisj  7101  cc3  7442  seq3f1olemstep  10723  seq3f1olemp  10724  nfsum1  11853  sumeq2  11856  sumfct  11871  sumrbdclem  11874  summodclem3  11877  summodclem2a  11878  zsumdc  11881  fsumgcl  11883  fsum3  11884  isumss  11888  isumss2  11890  fsum3cvg2  11891  fsumzcl2  11902  fsumsplitf  11905  sumsnf  11906  sumsns  11912  fsumsplitsnun  11916  fsum2dlemstep  11931  fisumcom2  11935  fsumshftm  11942  fisum0diag2  11944  fsummulc2  11945  fsum00  11959  fsumabs  11962  fsumrelem  11968  fsumiun  11974  isumshft  11987  mertenslem2  12033  nfcprod1  12051  prodeq2  12054  prodrbdclem  12068  prodmodclem3  12072  prodmodclem2a  12073  zproddc  12076  fprodseq  12080  fprodntrivap  12081  prodfct  12084  prodssdc  12086  fprodmul  12088  prodsnf  12089  fprodm1s  12098  fprodp1s  12099  prodsns  12100  fprodcl2lem  12102  fprodcllemf  12110  fprodabs  12113  fprodap0  12118  fprod2dlemstep  12119  fprodcom2fi  12123  fprodrec  12126  fproddivapf  12128  fprodsplitf  12129  fprodsplit1f  12131  fprodap0f  12133  fprodle  12137  fprodmodd  12138  pcmpt  12852  pcmptdvds  12854  ctiunctlemudc  12994  ctiunctlemf  12995  ctiunct  12997  ctiunctal  12998  gsumfzfsumlemm  14536  iuncld  14774  fsumcncntop  15226  limcmpted  15322  dvmptfsum  15384  fsumdvdsmul  15650