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

Theorem nfe1 1428
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 1427 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1394 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1392   E.wex 1424
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 1381  ax-ie1 1425
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  nf3  1602  sb4or  1758  nfmo1  1957  euexex  2030  2moswapdc  2035  nfre1  2415  ceqsexg  2736  morex  2790  sbc6g  2853  rgenm  3371  intab  3700  nfopab1  3882  nfopab2  3883  copsexg  4045  copsex2t  4046  copsex2g  4047  eusv2nf  4252  onintonm  4307  mosubopt  4471  dmcoss  4670  imadif  5059  funimaexglem  5062  nfoprab1  5655  nfoprab2  5656  nfoprab3  5657  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773
  Copyright terms: Public domain W3C validator