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

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

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1472 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1439 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1437  wex 1469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ie1 1470
This theorem depends on definitions:  df-bi 116  df-nf 1438
This theorem is referenced by:  nf3  1648  sb4or  1806  nfmo1  2012  euexex  2085  2moswapdc  2090  nfre1  2477  ceqsexg  2814  morex  2869  sbc6g  2934  rgenm  3466  intab  3804  nfopab1  4001  nfopab2  4002  copsexg  4170  copsex2t  4171  copsex2g  4172  eusv2nf  4381  onintonm  4437  mosubopt  4608  dmcoss  4812  imadif  5207  funimaexglem  5210  nfoprab1  5824  nfoprab2  5825  nfoprab3  5826  exmidfodomrlemr  7071  exmidfodomrlemrALT  7072
  Copyright terms: Public domain W3C validator