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

Theorem nfcsb1v 2910
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  |-  F/_ x [_ A  /  x ]_ B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2194 . 2  |-  F/_ x A
21nfcsb1 2909 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2181   [_csb 2880
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-sbc 2788  df-csb 2881
This theorem is referenced by:  csbhypf  2913  csbiebt  2914  sbcnestgf  2925  csbnest1g  2929  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  csbing  3172  sbcbrg  3841  moop2  4016  pofun  4077  eusvnf  4213  opeliunxp  4423  elrnmpt1  4613  csbima12g  4714  fvmpts  5278  fvmpt2  5282  mptfvex  5284  fmptco  5358  fmptcof  5359  fmptcos  5360  elabrex  5425  fliftfuns  5466  csbov123g  5571  ovmpt2s  5652  mpt2mptsx  5851  dmmpt2ssx  5853  fmpt2x  5854  mpt2fvex  5857  fmpt2co  5865  dfmpt2  5872  f1od2  5884  eqerlem  6168  qliftfuns  6221  nfsum1  10106
  Copyright terms: Public domain W3C validator