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

Theorem nfa1 1486
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 1485 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1403 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1294   F/wnf 1401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1390  ax-ial 1479
This theorem depends on definitions:  df-bi 116  df-nf 1402
This theorem is referenced by:  nfnf1  1488  nfa2  1523  nfia1  1524  alexdc  1562  nf2  1610  cbv1h  1687  sbf2  1715  sb4or  1768  nfsbxy  1873  nfsbxyt  1874  sbcomxyyz  1901  sbalyz  1930  dvelimALT  1941  nfeu1  1966  moim  2019  euexex  2040  nfaba1  2241  nfra1  2420  ceqsalg  2661  elrab3t  2784  mo2icl  2808  csbie2t  2990  sbcnestgf  2993  dfss4st  3248  dfnfc2  3693  mpteq12f  3940  copsex2t  4096  ssopab2  4126  alxfr  4311  eunex  4405  mosubopt  4532  fv3  5363  fvmptt  5430  fnoprabg  5784  fiintim  6719  bj-exlimmp  12378  bdsepnft  12486  setindft  12568  strcollnft  12587
  Copyright terms: Public domain W3C validator