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  2088  nfs1  2100  sb6f  2122  hbsb  2186  nfsab  2428  nfcrii  2565  bnj1316  29192  bnj1379  29202  bnj1468  29217  bnj958  29311  bnj981  29321  bnj1014  29331  bnj1128  29359  bnj1204  29381  bnj1279  29387  bnj1398  29403  bnj1408  29405  bnj1444  29412  bnj1445  29413  bnj1446  29414  bnj1447  29415  bnj1448  29416  bnj1449  29417  bnj1463  29424  bnj1312  29427  bnj1518  29433  bnj1519  29434  bnj1520  29435  bnj1525  29438  nfalwAUX7  29450  equsalNEW7  29487  cbvaldwAUX7  29515  cbv3dwAUX7  29516  nfs1NEW7  29545  equs45fNEW7  29621  sb6fNEW7  29633  ax7nfAUX7  29655  dvelimfwAUX7  29664  nfalOLD7  29687  cbvaldOLD7  29734  hbsbOLD7  29749
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