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

Theorem nf5i 2022
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 2021 . 2 (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2 nf5i.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1722 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479  wnf 1706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-10 2017
This theorem depends on definitions:  df-bi 197  df-ex 1703  df-nf 1708
This theorem is referenced by:  nfe1  2025  nf5di  2117  19.9h  2118  19.21h  2119  19.23h  2120  equsexhv  2122  hban  2126  hb3an  2127  exlimih  2146  exlimdh  2147  nfal  2151  nfexOLD  2153  hbex  2154  nfa1OLD  2155  dvelimhw  2171  cbv3hv  2172  cbv3h  2264  equsalh  2292  equsexh  2293  nfae  2314  axc16i  2320  dvelimh  2334  nfs1  2363  sbh  2379  nfs1v  2435  hbsb  2439  sb7h  2452  nfsab1  2610  nfsab  2612  cleqh  2722  nfcii  2753  nfcri  2756  bnj596  30790  bnj1146  30836  bnj1379  30875  bnj1464  30888  bnj1468  30890  bnj605  30951  bnj607  30960  bnj916  30977  bnj964  30987  bnj981  30994  bnj983  30995  bnj1014  31004  bnj1123  31028  bnj1373  31072  bnj1417  31083  bnj1445  31086  bnj1463  31097  bnj1497  31102  bj-cbv3hv2  32703  bj-equsalhv  32719  bj-nfs1v  32734  bj-nfsab1  32747  bj-nfcri  32827  wl-nfalv  33283  nfequid-o  34014  nfa1-o  34019  2sb5ndVD  38966  2sb5ndALT  38988
  Copyright terms: Public domain W3C validator