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

Theorem nfi 1668
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 1662 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1667 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663
This theorem depends on definitions:  df-bi 188  df-nf 1662
This theorem is referenced by:  nfth  1670  nfnth  1673  nfv  1755  nfe1  1894  nfdh  1934  19.9h  1948  19.9hOLD  1950  nfa1  1956  19.21h  1966  19.23h  1971  exlimih  1973  exlimdh  1975  nfdi  1976  nfim1  1979  nfan1  1987  hban  1991  hb3an  1992  nfal  2007  nfex  2008  dvelimhw  2015  cbv3h  2074  equsalh  2094  equsexh  2097  nfae  2115  axc16i  2123  dvelimh  2137  nfs1  2161  sbh  2179  nfs1v  2236  hbsb  2240  sb7h  2253  nfsab1  2411  nfsab  2413  cleqh  2532  nfcii  2570  nfcri  2573  bnj596  29564  bnj1146  29611  bnj1379  29650  bnj1464  29663  bnj1468  29665  bnj605  29726  bnj607  29735  bnj916  29752  bnj964  29762  bnj981  29769  bnj983  29770  bnj1014  29779  bnj1123  29803  bnj1373  29847  bnj1417  29858  bnj1445  29861  bnj1463  29872  bnj1497  29877  bj-cbv3hv  31290  bj-cbv3hv2  31291  bj-equsalhv  31310  bj-equsexhv  31313  bj-nfs1v  31352  bj-nfsab1  31356  bj-nfdiOLD  31414  bj-nfcri  31431  wl-nfalv  31821  nfequid-o  32450  nfa1-o  32455  2sb5ndVD  37280  2sb5ndALT  37302
  Copyright terms: Public domain W3C validator