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

Theorem nfi 1541
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 1535 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1540 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfth  1543  nfnth  1546  nfv  1609  nfe1  1718  nfdh  1759  nfa1  1768  nfal  1778  exlimdh  1816  nfim1  1833  nfan1  1834  nfae  1907  equsalh  1914  equsexh  1916  sbh  1980  nfs1  1997  ax16i  1999  nfs1v  2058  hbsb  2062  sb7h  2073  nfequid-o  2113  nfa1-o  2118  nfsab1  2286  nfsab  2288  nfcii  2423  nfcri  2426  riotasvdOLD  6364  riotasv2dOLD  6366  riotasv3dOLD  6370  disjorf  23371  2sb5ndVD  29002  2sb5ndALT  29025  bnj596  29091  bnj1131  29135  bnj1146  29139  bnj1379  29179  bnj1397  29183  bnj1464  29192  bnj1468  29194  bnj605  29255  bnj607  29264  bnj916  29281  bnj964  29291  bnj981  29298  bnj983  29299  bnj1014  29308  bnj1123  29332  bnj1145  29339  bnj1373  29376  bnj1417  29387  bnj1445  29390  bnj1463  29401  bnj1497  29406  nfalwAUX7  29427  nfaewAUX7  29457  nfaew2AUX7  29460  equsalhNEW7  29466  equsexhNEW7  29468  nfaew3AUX7  29500  nfs1NEW7  29520  ax16iNEW7  29526  sbhNEW7  29534  sbco3wAUX7  29561  sbcomwAUX7  29562  nfs1vNEW7  29578  nfalOLD7  29641  nfaeOLD7  29663  hbsbOLD7  29703  sb7hOLD7  29721
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator