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

Theorem nfa1 1450
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 1449 . 2  |-  ( A. x ph  ->  A. x A. x ph )
21nfi 1367 1  |-  F/ x A. x ph
Colors of variables: wff set class
Syntax hints:   A.wal 1257   F/wnf 1365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  nfnf1  1452  nfa2  1487  nfia1  1488  alexdc  1526  nf2  1574  cbv1h  1649  sbf2  1677  sb4or  1730  nfsbxy  1834  nfsbxyt  1835  sbcomxyyz  1862  sbalyz  1891  dvelimALT  1902  nfeu1  1927  moim  1980  euexex  2001  nfaba1  2199  nfra1  2372  ceqsalg  2599  elrab3t  2720  mo2icl  2743  csbie2t  2922  sbcnestgf  2925  dfnfc2  3626  mpteq12f  3865  copsex2t  4010  ssopab2  4040  alxfr  4221  eunex  4313  mosubopt  4433  fv3  5225  fvmptt  5290  fnoprabg  5630  bj-exlimmp  10296  bdsepnft  10394  setindft  10477  strcollnft  10496
  Copyright terms: Public domain W3C validator