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

Theorem nfs1v 1815
 Description: is not free in when and are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfs1v
Distinct variable group:   ,
Allowed substitution hints:   (,)

Proof of Theorem nfs1v
StepHypRef Expression
1 hbs1 1814 . 2
21nfi 1351 1
 Colors of variables: wff set class Syntax hints:  wnf 1349  wsb 1645 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-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646 This theorem is referenced by:  nfsbxy  1818  nfsbxyt  1819  sbco3v  1843  sbcomxyyz  1846  sbnf2  1857  mo2n  1928  mo23  1941  mor  1942  clelab  2162  cbvralf  2527  cbvrexf  2528  cbvralsv  2544  cbvrexsv  2545  cbvrab  2555  sbhypf  2603  mob2  2721  reu2  2729  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  sbcel12g  2865  sbceqg  2866  cbvreucsf  2910  cbvrabcsf  2911  cbvopab1  3830  cbvopab1s  3832  csbopabg  3835  cbvmpt  3851  opelopabsb  3997  frind  4089  tfis  4306  findes  4326  opeliunxp  4395  ralxpf  4482  rexxpf  4483  cbviota  4872  csbiotag  4895  isarep1  4985  cbvriota  5478  csbriotag  5480  abrexex2g  5747  abrexex2  5751  dfoprab4f  5819  uzind4s  8533  cbvrald  9927  bj-bdfindes  10074  bj-findes  10106
 Copyright terms: Public domain W3C validator