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

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

Proof of Theorem nfa1
StepHypRef Expression
1 hba1 1476 . 2 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)
21nfi 1394 1 𝑥𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wal 1285  wnf 1392
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-ial 1470
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  nfnf1  1479  nfa2  1514  nfia1  1515  alexdc  1553  nf2  1601  cbv1h  1677  sbf2  1705  sb4or  1758  nfsbxy  1863  nfsbxyt  1864  sbcomxyyz  1891  sbalyz  1920  dvelimALT  1931  nfeu1  1956  moim  2009  euexex  2030  nfaba1  2230  nfra1  2405  ceqsalg  2641  elrab3t  2761  mo2icl  2785  csbie2t  2965  sbcnestgf  2968  dfss4st  3221  dfnfc2  3656  mpteq12f  3895  copsex2t  4048  ssopab2  4078  alxfr  4259  eunex  4352  mosubopt  4473  fv3  5293  fvmptt  5359  fnoprabg  5705  bj-exlimmp  11139  bdsepnft  11247  setindft  11329  strcollnft  11348
  Copyright terms: Public domain W3C validator