ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcsb1v Structured version   GIF version

Theorem nfcsb1v 2859
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 xA / xB
Distinct variable group:   x,A
Allowed substitution hint:   B(x)

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2160 . 2 xA
21nfcsb1 2858 1 xA / xB
Colors of variables: wff set class
Syntax hints:  wnfc 2147  csb 2829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-sbc 2742  df-csb 2830
This theorem is referenced by:  csbhypf  2862  csbiebt  2863  sbcnestgf  2874  csbnest1g  2878  cbvralcsf  2885  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  csbing  3121  sbcbrg  3787  moop2  3962  pofun  4023  eusvnf  4135  opeliunxp  4322  elrnmpt1  4512  csbima12g  4613  fvmpts  5175  fvmpt2  5179  mptfvex  5181  fmptco  5255  fmptcof  5256  fmptcos  5257  elabrex  5322  fliftfuns  5363  csbov123g  5466  ovmpt2s  5547  mpt2mptsx  5746  dmmpt2ssx  5748  fmpt2x  5749  mpt2fvex  5752  fmpt2co  5760  dfmpt2  5767  eqerlem  6048  qliftfuns  6101
  Copyright terms: Public domain W3C validator