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

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

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1439 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1406 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1404  wex 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-ie1 1437
This theorem depends on definitions:  df-bi 116  df-nf 1405
This theorem is referenced by:  nf3  1615  sb4or  1772  nfmo1  1972  euexex  2045  2moswapdc  2050  nfre1  2435  ceqsexg  2767  morex  2821  sbc6g  2886  rgenm  3412  intab  3747  nfopab1  3937  nfopab2  3938  copsexg  4104  copsex2t  4105  copsex2g  4106  eusv2nf  4315  onintonm  4371  mosubopt  4542  dmcoss  4744  imadif  5139  funimaexglem  5142  nfoprab1  5752  nfoprab2  5753  nfoprab3  5754  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968
  Copyright terms: Public domain W3C validator