Theorem nfcsb1v 2977

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

Syntax hints:  Ⅎwnfc 2222  ⦋csb 2947

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-sbc 2855  df-csb 2948

This theorem is referenced by:  csbhypf  2980  csbiebt  2981  sbcnestgf  2993  csbnest1g  2997  cbvralcsf  3004  cbvrexcsf  3005  cbvreucsf  3006  cbvrabcsf  3007  csbing  3222  disjnims  3859  disjiun  3862  sbcbrg  3916  moop2  4102  pofun  4163  eusvnf  4303  opeliunxp  4522  elrnmpt1  4718  resmptf  4795  csbima12g  4826  fvmpts  5417  fvmpt2  5422  mptfvex  5424  fmptco  5503  fmptcof  5504  fmptcos  5505  elabrex  5575  fliftfuns  5615  csbov123g  5725  ovmpt2s  5806  mpt2mptsx  6005  dmmpt2ssx  6007  fmpt2x  6008  mpt2fvex  6011  fmpt2co  6019  dfmpt2  6026  f1od2  6038  disjxp1  6039  eqerlem  6363  qliftfuns  6416  mptelixpg  6531  xpf1o  6640  iunfidisj  6735  seq3f1olemstep  10067  seq3f1olemp  10068  nfsum1  10915  sumeq2  10918  sumfct  10933  sumrbdclem  10935  summodclem3  10939  summodclem2a  10940  zsumdc  10943  fsumgcl  10945  fsum3  10946  isumss  10950  isumss2  10952  fsum3cvg2  10953  fsumzcl2  10964  fsumsplitf  10967  sumsnf  10968  sumsns  10974  fsumsplitsnun  10978  fsum2dlemstep  10993  fisumcom2  10997  fsumshftm  11004  fisum0diag2  11006  fsummulc2  11007  fsum00  11021  fsumabs  11024  fsumrelem  11030  fsumiun  11036  isumshft  11049  mertenslem2  11095  iuncld  11983