MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfi Structured version   Visualization version   Unicode version

Theorem nfi 1685
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 1679 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1684 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1453   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680
This theorem depends on definitions:  df-bi 190  df-nf 1679
This theorem is referenced by:  nfth  1687  nfnth  1690  nfv  1772  nfe1  1929  nfdh  1968  19.9h  1982  19.9hOLD  1984  nfa1  1990  19.21h  2000  19.23h  2005  exlimih  2007  exlimdh  2009  nfdi  2010  nfim1  2013  nfan1  2021  hban  2025  hb3an  2026  nfal  2041  nfex  2042  dvelimhw  2071  cbv3hv  2072  equsexhv  2078  cbv3h  2120  equsalh  2140  equsexh  2143  nfae  2161  axc16i  2167  dvelimh  2181  nfs1  2205  sbh  2221  nfs1v  2277  hbsb  2281  sb7h  2294  nfsab1  2452  nfsab  2454  cleqh  2563  nfcii  2594  nfcri  2597  bnj596  29606  bnj1146  29653  bnj1379  29692  bnj1464  29705  bnj1468  29707  bnj605  29768  bnj607  29777  bnj916  29794  bnj964  29804  bnj981  29811  bnj983  29812  bnj1014  29821  bnj1123  29845  bnj1373  29889  bnj1417  29900  bnj1445  29903  bnj1463  29914  bnj1497  29919  bj-cbv3hv2  31375  bj-equsalhv  31392  bj-nfs1v  31429  bj-nfsab1  31433  bj-nfdiOLD  31490  bj-nfcri  31507  wl-nfalv  31903  nfequid-o  32527  nfa1-o  32532  2sb5ndVD  37348  2sb5ndALT  37370
  Copyright terms: Public domain W3C validator