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

Theorem nfe1 1457
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 1456 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1423 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1421   E.wex 1453
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 1410  ax-ie1 1454
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  nf3  1632  sb4or  1789  nfmo1  1989  euexex  2062  2moswapdc  2067  nfre1  2453  ceqsexg  2787  morex  2841  sbc6g  2906  rgenm  3435  intab  3770  nfopab1  3967  nfopab2  3968  copsexg  4136  copsex2t  4137  copsex2g  4138  eusv2nf  4347  onintonm  4403  mosubopt  4574  dmcoss  4778  imadif  5173  funimaexglem  5176  nfoprab1  5788  nfoprab2  5789  nfoprab3  5790  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027
  Copyright terms: Public domain W3C validator