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

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

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1495 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1462 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1460  wex 1492
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 1449  ax-ie1 1493
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  nf3  1669  sb4or  1833  nfmo1  2038  euexex  2111  2moswapdc  2116  nfre1  2520  ceqsexg  2865  morex  2921  sbc6g  2987  rgenm  3525  intab  3871  nfopab1  4069  nfopab2  4070  copsexg  4241  copsex2t  4242  copsex2g  4243  eusv2nf  4453  onintonm  4513  mosubopt  4688  dmcoss  4892  imadif  5292  funimaexglem  5295  nfoprab1  5918  nfoprab2  5919  nfoprab3  5920  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  dfgrp3mlem  12854
  Copyright terms: Public domain W3C validator