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

Theorem nfi 1421
Description: Deduce that  x is not free in  ph from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfi.1  |-  ( ph  ->  A. x ph )
Assertion
Ref Expression
nfi  |-  F/ x ph

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1420 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1412 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312   F/wnf 1419
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 1408
This theorem depends on definitions:  df-bi 116  df-nf 1420
This theorem is referenced by:  nfth  1423  nfnth  1424  nfe1  1455  nfdh  1487  nfv  1491  nfa1  1504  nfan1  1526  nfim1  1533  nfor  1536  nfal  1538  nfex  1599  nfae  1680  cbv3h  1704  nfs1  1763  nfs1v  1890  hbsb  1898  sbco2h  1913  hbsbd  1933  dvelimALT  1961  dvelimfv  1962  hbeu  1996  hbeud  1997  eu3h  2020  mo3h  2028  nfsab1  2105  nfsab  2107  nfcii  2247  nfcri  2250
  Copyright terms: Public domain W3C validator