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

Theorem nfnf1 1809
Description:  x is not free in  F/ x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfnf1  |-  F/ x F/ x ph

Proof of Theorem nfnf1
StepHypRef Expression
1 df-nf 1555 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfa1 1807 . 2  |-  F/ x A. x ( ph  ->  A. x ph )
31, 2nfxfr 1580 1  |-  F/ x F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550   F/wnf 1554
This theorem is referenced by:  nfnd  1810  nfndOLD  1811  nfimd  1828  19.23tOLD  1839  nfald  1872  nfaldOLD  1873  spimtOLD  1957  spimedOLD  1962  ax12olem3  2008  nfsb4t  2129  nfnfc1  2577  sbcnestgf  3300  dfnfc2  4035  nfaldwAUX7  29514  spimtNEW7  29569  spimedNEW7  29572  nfaldOLD7  29752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator