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

Theorem nf5i 2084
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 2083 . 2 (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2 nf5i.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1760 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1505  wnf 1746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-10 2079
This theorem depends on definitions:  df-bi 199  df-ex 1743  df-nf 1747
This theorem is referenced by:  nfe1  2087  sbh  2201  nf5di  2219  19.9h  2220  19.21h  2221  19.23h  2222  exlimih  2223  exlimdh  2224  equsalhw  2225  equsexhv  2226  hban  2234  hb3an  2235  nfal  2263  hbex  2265  cbv3hv  2276  dvelimhw  2279  cbv3h  2337  equsalh  2355  equsexh  2356  nfae  2369  axc16i  2372  dvelimh  2386  nfs1  2448  hbsb  2489  sb7h  2492  nfsab1OLD  2768  nfsab  2770  cleqh  2889  nfcii  2920  nfcri  2926  bnj596  31671  bnj1146  31717  bnj1379  31756  bnj1464  31769  bnj1468  31771  bnj605  31832  bnj607  31841  bnj916  31858  bnj964  31868  bnj981  31875  bnj983  31876  bnj1014  31885  bnj1123  31909  bnj1373  31953  bnj1417  31964  bnj1445  31967  bnj1463  31978  bnj1497  31983  bj-cbv3hv2  33581  bj-equsalhv  33595  bj-nfs1v  33605  bj-nfsab1  33610  wl-nfalv  34214  nfequid-o  35497  nfa1-o  35502  2sb5ndVD  40669  2sb5ndALT  40691
  Copyright terms: Public domain W3C validator