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

Theorem nfe1 1426
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 1425 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1392 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1390   E.wex 1422
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 1379  ax-ie1 1423
This theorem depends on definitions:  df-bi 115  df-nf 1391
This theorem is referenced by:  nf3  1600  sb4or  1756  nfmo1  1955  euexex  2028  2moswapdc  2033  nfre1  2413  ceqsexg  2733  morex  2787  sbc6g  2850  rgenm  3365  intab  3691  nfopab1  3873  nfopab2  3874  copsexg  4034  copsex2t  4035  copsex2g  4036  eusv2nf  4241  onintonm  4296  mosubopt  4460  dmcoss  4659  imadif  5046  funimaexglem  5049  nfoprab1  5632  nfoprab2  5633  nfoprab3  5634  exmidfodomrlemr  6730  exmidfodomrlemrALT  6731
  Copyright terms: Public domain W3C validator