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

Theorem nfe1 1401
Description: 𝑥 is not free in 𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfe1 𝑥𝑥𝜑

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1400 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1367 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1365  wex 1397
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-gen 1354  ax-ie1 1398
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  nf3  1575  sb4or  1730  nfmo1  1928  euexex  2001  2moswapdc  2006  nfre1  2382  ceqsexg  2695  morex  2748  sbc6g  2811  rgenm  3351  intab  3672  nfopab1  3854  nfopab2  3855  copsexg  4009  copsex2t  4010  copsex2g  4011  eusv2nf  4216  onintonm  4271  mosubopt  4433  dmcoss  4629  imadif  5007  funimaexglem  5010  nfoprab1  5582  nfoprab2  5583  nfoprab3  5584
  Copyright terms: Public domain W3C validator