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

Theorem nf5i 2190
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 2189 . 2 (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2 nf5i.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1879 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-10 2185
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864
This theorem is referenced by:  nfe1  2194  nf5di  2294  19.9h  2295  19.21h  2296  19.23h  2297  equsalhw  2298  equsexhv  2300  hban  2304  hb3an  2305  exlimih  2325  exlimdh  2326  nfal  2329  nfexOLD  2331  hbex  2332  nfa1OLD  2333  cbv3hv  2347  dvelimhw  2350  cbv3h  2439  equsalh  2461  equsexh  2462  nfae  2480  axc16i  2484  dvelimh  2498  nfs1  2524  sbh  2540  nfs1vOLD  2590  hbsb  2603  sb7h  2614  nfsab1  2794  nfsab  2796  cleqh  2906  nfcii  2937  nfcri  2940  bnj596  31137  bnj1146  31183  bnj1379  31222  bnj1464  31235  bnj1468  31237  bnj605  31298  bnj607  31307  bnj916  31324  bnj964  31334  bnj981  31341  bnj983  31342  bnj1014  31351  bnj1123  31375  bnj1373  31419  bnj1417  31430  bnj1445  31433  bnj1463  31444  bnj1497  31449  bj-cbv3hv2  33040  bj-equsalhv  33056  bj-nfs1v  33071  bj-nfsab1  33084  wl-nfalv  33624  nfequid-o  34687  nfa1-o  34692  2sb5ndVD  39638  2sb5ndALT  39660
  Copyright terms: Public domain W3C validator