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

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

Proof of Theorem nfa1
StepHypRef Expression
1 hba1 1520 . 2 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1438 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wal 1329  wnf 1436
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 1425  ax-ial 1514
This theorem depends on definitions:  df-bi 116  df-nf 1437
This theorem is referenced by:  nfnf1  1523  nfa2  1558  nfia1  1559  alexdc  1598  nf2  1646  cbv1h  1723  sbf2  1751  sb4or  1805  nfsbxy  1915  nfsbxyt  1916  sbcomxyyz  1945  sbalyz  1974  dvelimALT  1985  nfeu1  2010  moim  2063  euexex  2084  nfaba1  2287  nfra1  2466  ceqsalg  2714  elrab3t  2839  mo2icl  2863  csbie2t  3048  sbcnestgf  3051  dfss4st  3309  dfnfc2  3754  mpteq12f  4008  copsex2t  4167  ssopab2  4197  alxfr  4382  eunex  4476  mosubopt  4604  fv3  5444  fvmptt  5512  fnoprabg  5872  fiintim  6817  bj-exlimmp  13006  bdsepnft  13115  setindft  13193  strcollnft  13212
  Copyright terms: Public domain W3C validator