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

Theorem nfe1 1366
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 1365 . 2 (xφxxφ)
21nfi 1331 1 xxφ
Colors of variables: wff set class
Syntax hints:  wnf 1329  wex 1362
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 1318  ax-ie1 1363
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  nf3  1541  sb4or  1696  nfmo1  1894  euexex  1967  2moswapdc  1972  nfre1  2343  ceqsexg  2649  morex  2702  sbc6g  2765  rgenm  3302  intab  3618  nfopab1  3800  nfopab2  3801  copsexg  3955  copsex2t  3956  copsex2g  3957  eusv2nf  4138  mosubopt  4332  dmcoss  4528  imadif  4905  funimaexglem  4908  nfoprab1  5477  nfoprab2  5478  nfoprab3  5479
  Copyright terms: Public domain W3C validator