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

Theorem nfi 1597
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 1591 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1596 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592
This theorem depends on definitions:  df-bi 185  df-nf 1591
This theorem is referenced by:  nfth  1599  nfnth  1602  nfv  1674  nfe1  1780  nfdh  1815  19.9h  1827  nfa1  1833  19.21h  1842  19.23h  1846  exlimih  1848  exlimdh  1850  nfdi  1851  nfim1  1854  nfan1  1862  hban  1866  hb3an  1867  nfal  1882  nfex  1883  dvelimhw  1890  nfdiOLD  1900  cbv3h  1969  equsalh  1994  equsexh  1996  nfae  2013  axc16i  2021  dvelimh  2035  nfs1  2061  sbh  2079  nfs1v  2149  hbsb  2154  sb7h  2171  nfequid-o  2218  nfa1-o  2223  nfsab1  2440  nfsab  2442  cleqh  2566  nfcii  2603  nfcri  2606  2sb5ndVD  31946  2sb5ndALT  31968  bnj596  32038  bnj1146  32085  bnj1379  32124  bnj1464  32137  bnj1468  32139  bnj605  32200  bnj607  32209  bnj916  32226  bnj964  32236  bnj981  32243  bnj983  32244  bnj1014  32253  bnj1123  32277  bnj1145  32284  bnj1373  32321  bnj1417  32332  bnj1445  32335  bnj1463  32346  bnj1497  32351  bj-cbv3hv  32526  bj-cbv3hv2  32527  bj-equsalhv  32547  bj-equsexhv  32549  bj-nfs1v  32588  bj-nfsab1  32592  bj-nfcri  32663
  Copyright terms: Public domain W3C validator