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

Theorem nfi 1538
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 1532 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1537 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfth  1540  nfnth  1543  nfv  1605  nfe1  1706  nfdh  1747  nfa1  1756  nfal  1766  exlimdh  1804  nfim1  1821  nfan1  1822  nfae  1894  equsalh  1901  equsexh  1903  sbh  1967  nfs1  1984  ax16i  1986  nfs1v  2045  hbsb  2049  sb7h  2060  nfequid-o  2100  nfa1-o  2105  nfsab1  2273  nfsab  2275  nfcii  2410  nfcri  2413  riotasvdOLD  6348  riotasv2dOLD  6350  riotasv3dOLD  6354  disjorf  23356  2sb5ndVD  28686  2sb5ndALT  28709  bnj596  28775  bnj1131  28819  bnj1146  28823  bnj1379  28863  bnj1397  28867  bnj1464  28876  bnj1468  28878  bnj605  28939  bnj607  28948  bnj916  28965  bnj964  28975  bnj981  28982  bnj983  28983  bnj1014  28992  bnj1123  29016  bnj1145  29023  bnj1373  29060  bnj1417  29071  bnj1445  29074  bnj1463  29085  bnj1497  29090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator