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

Theorem nfe1 1473
Description:  x is not free in  E. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfe1  |-  F/ x E. x ph

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1472 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1439 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1437   E.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  2479  ceqsexg  2816  morex  2871  sbc6g  2936  rgenm  3469  intab  3807  nfopab1  4004  nfopab2  4005  copsexg  4173  copsex2t  4174  copsex2g  4175  eusv2nf  4384  onintonm  4440  mosubopt  4611  dmcoss  4815  imadif  5210  funimaexglem  5213  nfoprab1  5827  nfoprab2  5828  nfoprab3  5829  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075
  Copyright terms: Public domain W3C validator