NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfi GIF version

Theorem nfi 1551
Description: Deduce that x is not free in φ from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfi.1 (φxφ)
Assertion
Ref Expression
nfi xφ

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1545 . 2 (Ⅎxφx(φxφ))
2 nfi.1 . 2 (φxφ)
31, 2mpgbir 1550 1 xφ
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wnf 1544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546
This theorem depends on definitions:  df-bi 177  df-nf 1545
This theorem is referenced by:  nfth  1553  nfnth  1556  nfv  1619  nfe1  1732  nfdh  1767  19.9h  1780  nfa1  1788  19.21h  1797  19.23h  1802  exlimih  1804  exlimdh  1807  nfim1  1811  nfim1OLD  1812  hban  1828  hb3an  1830  nfal  1842  nfex  1843  nfan1  1881  nfae  1954  equsalh  1961  equsexh  1963  sbh  2027  nfs1  2044  ax16i  2046  nfs1v  2106  hbsb  2110  sb7h  2121  nfequid-o  2161  nfa1-o  2166  nfsab1  2343  nfsab  2345  nfcii  2480  nfcri  2483
  Copyright terms: Public domain W3C validator