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

Theorem nfi 1462
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 1461 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1453 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1351   F/wnf 1460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  nfth  1464  nfnth  1465  nfe1  1496  nfdh  1524  nfv  1528  nfa1  1541  nfan1  1564  nfim1  1571  nfor  1574  nfex  1637  nfae  1719  cbv3h  1743  nfs1  1809  nfs1v  1939  hbsb  1949  sbco2h  1964  hbsbd  1982  dvelimALT  2010  dvelimfv  2011  hbeu  2047  hbeud  2048  eu3h  2071  mo3h  2079  nfsab1  2167  nfsab  2169  nfcii  2310  nfcri  2313
  Copyright terms: Public domain W3C validator