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

Theorem nf5i 2021
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 2020 . 2 (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2 nf5i.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1721 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-10 2016
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfe1  2024  nf5di  2116  19.9h  2117  19.21h  2118  19.23h  2119  hban  2124  hb3an  2125  exlimih  2144  exlimdh  2145  equsexhv  2146  nfal  2150  nfexOLD  2152  hbex  2153  nfa1OLD  2154  dvelimhw  2170  cbv3hv  2171  cbv3h  2265  equsalh  2291  equsexh  2294  nfae  2315  axc16i  2321  dvelimh  2335  nfs1  2364  sbh  2380  nfs1v  2436  hbsb  2440  sb7h  2453  nfsab1  2611  nfsab  2613  cleqh  2721  nfcii  2752  nfcri  2755  bnj596  30524  bnj1146  30570  bnj1379  30609  bnj1464  30622  bnj1468  30624  bnj605  30685  bnj607  30694  bnj916  30711  bnj964  30721  bnj981  30728  bnj983  30729  bnj1014  30738  bnj1123  30762  bnj1373  30806  bnj1417  30817  bnj1445  30820  bnj1463  30831  bnj1497  30836  bj-cbv3hv2  32370  bj-equsalhv  32387  bj-nfs1v  32402  bj-nfsab1  32415  bj-nfdiOLD  32474  bj-nfcri  32499  wl-nfalv  32944  nfequid-o  33675  nfa1-o  33680  2sb5ndVD  38629  2sb5ndALT  38651
  Copyright terms: Public domain W3C validator