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

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

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1506 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1473 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1471  wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie1 1504
This theorem depends on definitions:  df-bi 117  df-nf 1472
This theorem is referenced by:  nf3  1680  sb4or  1844  nfmo1  2050  euexex  2123  2moswapdc  2128  nfre1  2533  ceqsexg  2880  morex  2936  sbc6g  3002  rgenm  3540  intab  3888  nfopab1  4087  nfopab2  4088  copsexg  4262  copsex2t  4263  copsex2g  4264  eusv2nf  4474  onintonm  4534  mosubopt  4709  dmcoss  4914  imadif  5315  funimaexglem  5318  nfoprab1  5946  nfoprab2  5947  nfoprab3  5948  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  dfgrp3mlem  13057
  Copyright terms: Public domain W3C validator