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

Theorem nfa1 1506
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 1505 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1423 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1314   F/wnf 1421
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 1410  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  nfnf1  1508  nfa2  1543  nfia1  1544  alexdc  1583  nf2  1631  cbv1h  1708  sbf2  1736  sb4or  1789  nfsbxy  1895  nfsbxyt  1896  sbcomxyyz  1923  sbalyz  1952  dvelimALT  1963  nfeu1  1988  moim  2041  euexex  2062  nfaba1  2264  nfra1  2443  ceqsalg  2688  elrab3t  2812  mo2icl  2836  csbie2t  3018  sbcnestgf  3021  dfss4st  3279  dfnfc2  3724  mpteq12f  3978  copsex2t  4137  ssopab2  4167  alxfr  4352  eunex  4446  mosubopt  4574  fv3  5412  fvmptt  5480  fnoprabg  5840  fiintim  6785  bj-exlimmp  12903  bdsepnft  13012  setindft  13090  strcollnft  13109
  Copyright terms: Public domain W3C validator