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

Theorem nfri 1778
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfri.1  |-  F/ x ph
Assertion
Ref Expression
nfri  |-  ( ph  ->  A. x ph )

Proof of Theorem nfri
StepHypRef Expression
1 nfri.1 . 2  |-  F/ x ph
2 nfr 1777 . 2  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
31, 2ax-mp 8 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549   F/wnf 1553
This theorem is referenced by:  alimd  1780  alrimi  1781  eximd  1786  nexd  1787  albid  1788  exbid  1789  19.3  1791  19.9  1797  stdpc5OLD  1817  nfim1  1830  hban  1850  hb3an  1852  nfal  1864  nfex  1865  cbv2  1980  cbvaldOLD  1987  equsalOLD  2000  equs45f  2084  nfs1  2096  sb6f  2127  hbsb  2185  nfsab  2427  nfcrii  2564  bnj1316  29129  bnj1379  29139  bnj1468  29154  bnj958  29248  bnj981  29258  bnj1014  29268  bnj1128  29296  bnj1204  29318  bnj1279  29324  bnj1398  29340  bnj1408  29342  bnj1444  29349  bnj1445  29350  bnj1446  29351  bnj1447  29352  bnj1448  29353  bnj1449  29354  bnj1463  29361  bnj1312  29364  bnj1518  29370  bnj1519  29371  bnj1520  29372  bnj1525  29375  nfalwAUX7  29387  equsalNEW7  29424  cbvaldwAUX7  29452  cbv3dwAUX7  29453  nfs1NEW7  29482  equs45fNEW7  29558  sb6fNEW7  29570  ax7nfAUX7  29592  dvelimfwAUX7  29601  nfalOLD7  29624  cbvaldOLD7  29671  hbsbOLD7  29686
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator