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

Theorem nfi 1606
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 1600 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1605 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601
This theorem depends on definitions:  df-bi 185  df-nf 1600
This theorem is referenced by:  nfth  1608  nfnth  1611  nfv  1683  nfe1  1789  nfdh  1827  19.9h  1839  nfa1  1845  19.21h  1854  19.23h  1858  exlimih  1860  exlimdh  1862  nfdi  1863  nfim1  1866  nfan1  1874  hban  1878  hb3an  1879  nfal  1894  nfex  1895  dvelimhw  1902  nfdiOLD  1912  cbv3h  1985  equsalh  2010  equsexh  2012  nfae  2029  axc16i  2037  dvelimh  2051  nfs1  2077  sbh  2095  nfs1v  2164  hbsb  2169  sb7h  2186  nfequid-o  2233  nfa1-o  2238  nfsab1  2456  nfsab  2458  cleqh  2582  nfcii  2619  nfcri  2622  wl-nfalv  29904  2sb5ndVD  33191  2sb5ndALT  33213  bnj596  33283  bnj1146  33330  bnj1379  33369  bnj1464  33382  bnj1468  33384  bnj605  33445  bnj607  33454  bnj916  33471  bnj964  33481  bnj981  33488  bnj983  33489  bnj1014  33498  bnj1123  33522  bnj1145  33529  bnj1373  33566  bnj1417  33577  bnj1445  33580  bnj1463  33591  bnj1497  33596  bj-cbv3hv  33773  bj-cbv3hv2  33774  bj-equsalhv  33794  bj-equsexhv  33796  bj-nfs1v  33835  bj-nfsab1  33839  bj-nfcri  33910
  Copyright terms: Public domain W3C validator