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

Theorem nfr 1769
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.)
Assertion
Ref Expression
nfr  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)

Proof of Theorem nfr
StepHypRef Expression
1 df-nf 1551 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 sp 1755 . 2  |-  ( A. x ( ph  ->  A. x ph )  -> 
( ph  ->  A. x ph ) )
31, 2sylbi 188 1  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546   F/wnf 1550
This theorem is referenced by:  nfri  1770  nfrd  1771  19.21t  1803  19.23t  1808  nfimd  1817  nfaldOLD  1865  spimt  2000  sbft  2051  nfaldwAUX7  28783  spimtNEW7  28838  sbftNEW7  28885  ax7wnftAUX7  28982  nfaldOLD7  28999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator