Theorem nfcsb1v 3161

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

Syntax hints:  Ⅎwnfc 2362  ⦋csb 3128

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-sbc 3033  df-csb 3129

This theorem is referenced by:  csbhypf  3167  csbiebt  3168  sbcnestgf  3180  csbnest1g  3184  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  rspc2vd  3197  csbing  3416  disjnims  4084  invdisjrab  4087  disjiun  4088  sbcbrg  4148  moop2  4350  pofun  4415  eusvnf  4556  opeliunxp  4787  elrnmpt1  4989  resmptf  5069  csbima12g  5104  fvmpts  5733  fvmpt2  5739  mptfvex  5741  fmptco  5821  fmptcof  5822  fmptcos  5823  elabrex  5908  elabrexg  5909  fliftfuns  5949  csbov123g  6067  ovmpos  6155  fvmpopr2d  6168  mpomptsx  6371  dmmpossx  6373  fmpox  6374  mpofvex  6379  fmpoco  6390  dfmpo  6397  f1od2  6409  disjxp1  6410  eqerlem  6776  qliftfuns  6831  mptelixpg  6946  xpf1o  7073  iunfidisj  7188  cc3  7530  seq3f1olemstep  10820  seq3f1olemp  10821  nfsum1  11977  sumeq2  11980  sumfct  11995  sumrbdclem  11999  summodclem3  12002  summodclem2a  12003  zsumdc  12006  fsumgcl  12008  fsum3  12009  isumss  12013  isumss2  12015  fsum3cvg2  12016  fsumzcl2  12027  fsumsplitf  12030  sumsnf  12031  sumsns  12037  fsumsplitsnun  12041  fsum2dlemstep  12056  fisumcom2  12060  fsumshftm  12067  fisum0diag2  12069  fsummulc2  12070  fsum00  12084  fsumabs  12087  fsumrelem  12093  fsumiun  12099  isumshft  12112  mertenslem2  12158  nfcprod1  12176  prodeq2  12179  prodrbdclem  12193  prodmodclem3  12197  prodmodclem2a  12198  zproddc  12201  fprodseq  12205  fprodntrivap  12206  prodfct  12209  prodssdc  12211  fprodmul  12213  prodsnf  12214  fprodm1s  12223  fprodp1s  12224  prodsns  12225  fprodcl2lem  12227  fprodcllemf  12235  fprodabs  12238  fprodap0  12243  fprod2dlemstep  12244  fprodcom2fi  12248  fprodrec  12251  fproddivapf  12253  fprodsplitf  12254  fprodsplit1f  12256  fprodap0f  12258  fprodle  12262  fprodmodd  12263  pcmpt  12977  pcmptdvds  12979  ctiunctlemudc  13119  ctiunctlemf  13120  ctiunct  13122  ctiunctal  13123  gsumfzfsumlemm  14663  iuncld  14906  fsumcncntop  15358  limcmpted  15454  dvmptfsum  15516  fsumdvdsmul  15785