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

Theorem nfi 1561
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 1555 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1560 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550   F/wnf 1554
This theorem is referenced by:  nfth  1563  nfnth  1566  nfv  1630  nfe1  1748  nfdh  1784  19.9h  1795  nfa1  1807  19.21h  1816  19.23h  1821  exlimih  1823  exlimdh  1827  nfim1  1831  nfim1OLD  1832  nfan1  1846  hban  1851  hb3an  1853  nfal  1865  nfex  1866  dvelimhw  1877  cbv3h  1973  equsalh  2002  equsexh  2005  nfae  2043  ax16i  2052  dvelimh  2072  nfs1  2102  sbh  2120  nfs1v  2184  hbsb  2188  sb7h  2199  nfequid-o  2240  nfa1-o  2245  nfsab1  2428  nfsab  2430  nfcii  2565  nfcri  2568  riotasvdOLD  6595  riotasv2dOLD  6597  riotasv3dOLD  6601  2sb5ndVD  29084  2sb5ndALT  29106  bnj596  29176  bnj1146  29224  bnj1379  29264  bnj1464  29277  bnj1468  29279  bnj605  29340  bnj607  29349  bnj916  29366  bnj964  29376  bnj981  29383  bnj983  29384  bnj1014  29393  bnj1123  29417  bnj1145  29424  bnj1373  29461  bnj1417  29472  bnj1445  29475  bnj1463  29486  bnj1497  29491  nfalwAUX7  29512  nfaewAUX7  29542  nfaew2AUX7  29545  equsalhNEW7  29551  equsexhNEW7  29553  nfaew3AUX7  29587  nfs1NEW7  29607  ax16iNEW7  29613  sbhNEW7  29621  sb8iwAUX7  29651  nfs1vNEW7  29668  nfalOLD7  29749  nfaeOLD7  29771  hbsbOLD7  29811  sb7hOLD7  29827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556
This theorem depends on definitions:  df-bi 179  df-nf 1555
  Copyright terms: Public domain W3C validator