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

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

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1429 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1396 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1394  wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-ie1 1427
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  nf3  1604  sb4or  1761  nfmo1  1960  euexex  2033  2moswapdc  2038  nfre1  2419  ceqsexg  2743  morex  2797  sbc6g  2862  rgenm  3380  intab  3712  nfopab1  3899  nfopab2  3900  copsexg  4062  copsex2t  4063  copsex2g  4064  eusv2nf  4269  onintonm  4324  mosubopt  4491  dmcoss  4690  imadif  5080  funimaexglem  5083  nfoprab1  5680  nfoprab2  5681  nfoprab3  5682  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808
  Copyright terms: Public domain W3C validator