MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nf5i Structured version   Visualization version   GIF version

Theorem nf5i 2135
Description: Deduce that 𝑥 is not free in 𝜑 from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nf5i.1 (𝜑 → ∀𝑥𝜑)
Assertion
Ref Expression
nf5i 𝑥𝜑

Proof of Theorem nf5i
StepHypRef Expression
1 nf5-1 2134 . 2 (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2 nf5i.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1792 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1532  wnf 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2130
This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779
This theorem is referenced by:  nfnaew  2138  nfnaewOLD  2139  nfe1  2140  sbh  2260  nf5di  2275  19.9h  2276  19.21h  2277  19.23h  2278  exlimih  2279  exlimdh  2280  equsalhw  2281  equsexhv  2282  hban  2290  hb3an  2291  nfal  2312  hbex  2314  nfsbv  2319  cbv3hv  2331  dvelimhw  2336  cbv3h  2398  equsalh  2414  equsexh  2415  nfae  2427  axc16i  2430  dvelimh  2444  nfs1  2482  hbsb  2518  sb7h  2520  nfsab  2716  nfsabg  2717  cleqh  2856  nfcii  2880  nfralw  3299  bnj596  34602  bnj1146  34647  bnj1379  34686  bnj1464  34700  bnj1468  34702  bnj605  34763  bnj607  34772  bnj916  34789  bnj964  34799  bnj981  34806  bnj983  34807  bnj1014  34817  bnj1123  34842  bnj1373  34886  bnj1417  34897  bnj1445  34900  bnj1463  34911  bnj1497  34916  bj-cbv3hv2  36511  bj-equsalhv  36522  bj-nfs1v  36529  bj-nfsab1  36532  bj-gabima  36657  wl-nfalv  37231  nfequid-o  38619  nfa1-o  38624  2sb5ndVD  44621  2sb5ndALT  44643
  Copyright terms: Public domain W3C validator