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

Theorem nfe1 1382
Description: x is not free in xφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfe1 xxφ

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1381 . 2 (xφxxφ)
21nfi 1348 1 xxφ
Colors of variables: wff set class
Syntax hints:  wnf 1346  wex 1378
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-gen 1335  ax-ie1 1379
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  nf3  1556  sb4or  1711  nfmo1  1909  euexex  1982  2moswapdc  1987  nfre1  2359  ceqsexg  2666  morex  2719  sbc6g  2782  rgenm  3317  intab  3635  nfopab1  3817  nfopab2  3818  copsexg  3972  copsex2t  3973  copsex2g  3974  eusv2nf  4154  mosubopt  4348  dmcoss  4544  imadif  4922  funimaexglem  4925  nfoprab1  5496  nfoprab2  5497  nfoprab3  5498
  Copyright terms: Public domain W3C validator