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

Theorem nf5i 2147
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 2146 . 2 (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2 nf5i.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1797 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfnaew  2150  nfe1  2151  sbh  2273  nf5di  2285  19.9h  2286  19.21h  2287  19.23h  2288  exlimih  2289  exlimdh  2290  equsalhw  2291  equsexhv  2292  hban  2300  hb3an  2301  nfal  2322  hbex  2324  nfsbv  2329  cbv3hv  2338  dvelimhw  2343  cbv3h  2402  equsalh  2418  equsexh  2419  nfae  2431  axc16i  2434  dvelimh  2448  nfs1  2486  hbsb  2522  sb7h  2524  nfsab  2719  nfsabg  2720  cleqh  2857  nfcii  2880  nfralw  3283  bnj596  34709  bnj1146  34754  bnj1379  34793  bnj1464  34807  bnj1468  34809  bnj605  34870  bnj607  34879  bnj916  34896  bnj964  34906  bnj981  34913  bnj983  34914  bnj1014  34924  bnj1123  34949  bnj1373  34993  bnj1417  35004  bnj1445  35007  bnj1463  35018  bnj1497  35023  bj-cbv3hv2  36756  bj-equsalhv  36767  bj-nfs1v  36774  bj-nfsab1  36777  bj-gabima  36901  wl-nfalv  37486  nfequid-o  38876  nfa1-o  38881  2sb5ndVD  44872  2sb5ndALT  44894
  Copyright terms: Public domain W3C validator