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 1799 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2142
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfnaew  2150  nfe1  2151  sbh  2270  nf5di  2289  19.9h  2290  19.21h  2291  19.23h  2292  exlimih  2293  exlimdh  2294  equsalhw  2295  equsexhv  2296  hban  2304  hb3an  2305  nfal  2331  hbex  2333  hbsbwOLD  2340  cbv3hv  2349  dvelimhw  2355  cbv3h  2413  equsalh  2431  equsexh  2432  nfae  2444  axc16i  2447  dvelimh  2461  nfs1  2506  hbsb  2544  sb7h  2546  nfsab1OLD  2786  nfsab  2789  nfsabg  2790  cleqh  2913  nfcii  2940  nfcriOLDOLDOLD  2950  bnj596  32127  bnj1146  32173  bnj1379  32212  bnj1464  32226  bnj1468  32228  bnj605  32289  bnj607  32298  bnj916  32315  bnj964  32325  bnj981  32332  bnj983  32333  bnj1014  32343  bnj1123  32368  bnj1373  32412  bnj1417  32423  bnj1445  32426  bnj1463  32437  bnj1497  32442  bj-cbv3hv2  34229  bj-equsalhv  34240  bj-nfs1v  34247  bj-nfsab1  34250  wl-nfalv  34927  nfequid-o  36203  nfa1-o  36208  2sb5ndVD  41611  2sb5ndALT  41633
  Copyright terms: Public domain W3C validator