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

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

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1517 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1484 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1482  wex 1514
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 1471  ax-ie1 1515
This theorem depends on definitions:  df-bi 117  df-nf 1483
This theorem is referenced by:  nf3  1691  sb4or  1855  nfmo1  2065  euexex  2138  2moswapdc  2143  nfre1  2548  ceqsexg  2900  morex  2956  sbc6g  3022  intab  3913  nfopab1  4112  nfopab2  4113  copsexg  4287  copsex2t  4288  copsex2g  4289  eusv2nf  4502  onintonm  4564  mosubopt  4739  dmcoss  4947  imadif  5353  funimaexglem  5356  nfoprab1  5993  nfoprab2  5994  nfoprab3  5995  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  dfgrp3mlem  13372
  Copyright terms: Public domain W3C validator