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

Theorem nfa1 1477
Description:  x is not free in  A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfa1  |-  F/ x A. x ph

Proof of Theorem nfa1
StepHypRef Expression
1 hba1 1476 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1394 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1285   F/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  3654  mpteq12f  3893  copsex2t  4046  ssopab2  4076  alxfr  4257  eunex  4350  mosubopt  4471  fv3  5291  fvmptt  5357  fnoprabg  5703  bj-exlimmp  11115  bdsepnft  11223  setindft  11305  strcollnft  11324
  Copyright terms: Public domain W3C validator