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

Theorem nfi 1646
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 1640 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1645 1  |-  F/ x ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1405   F/wnf 1639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641
This theorem depends on definitions:  df-bi 187  df-nf 1640
This theorem is referenced by:  nfth  1648  nfnth  1651  nfv  1730  nfe1  1866  nfdh  1905  19.9h  1919  19.9hOLD  1921  nfa1  1927  19.21h  1937  19.23h  1941  exlimih  1943  exlimdh  1945  nfdi  1946  nfim1  1949  nfan1  1957  hban  1961  hb3an  1962  nfal  1977  nfex  1978  dvelimhw  1985  nfdiOLD  1993  cbv3h  2045  equsalh  2065  equsexh  2067  nfae  2084  axc16i  2092  dvelimh  2106  nfs1  2130  sbh  2148  nfs1v  2207  hbsb  2211  sb7h  2224  nfsab1  2393  nfsab  2395  cleqh  2519  nfcii  2556  nfcri  2559  bnj596  29143  bnj1146  29190  bnj1379  29229  bnj1464  29242  bnj1468  29244  bnj605  29305  bnj607  29314  bnj916  29331  bnj964  29341  bnj981  29348  bnj983  29349  bnj1014  29358  bnj1123  29382  bnj1373  29426  bnj1417  29437  bnj1445  29440  bnj1463  29451  bnj1497  29456  bj-cbv3hv  30867  bj-cbv3hv2  30868  bj-equsalhv  30888  bj-equsexhv  30891  bj-nfs1v  30930  bj-nfsab1  30934  bj-nfcri  31005  wl-nfalv  31357  nfequid-o  31946  nfa1-o  31951  2sb5ndVD  36754  2sb5ndALT  36776
  Copyright terms: Public domain W3C validator