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

Theorem nf5i 2179
 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 2178 . 2 (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2 nf5i.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpg 1872 1 𝑥𝜑
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1629  Ⅎwnf 1856 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-10 2174 This theorem depends on definitions:  df-bi 197  df-ex 1853  df-nf 1858 This theorem is referenced by:  nfe1  2183  nf5di  2282  19.9h  2283  19.21h  2284  19.23h  2285  equsalhw  2286  equsexhv  2288  hban  2292  hb3an  2293  exlimih  2313  exlimdh  2314  nfal  2317  nfexOLD  2319  hbex  2320  nfa1OLD  2321  cbv3hv  2335  dvelimhw  2338  cbv3h  2427  equsalh  2449  equsexh  2450  nfae  2468  axc16i  2472  dvelimh  2486  nfs1  2512  sbh  2528  nfs1vOLD  2578  hbsb  2591  sb7h  2602  nfsab1  2761  nfsab  2763  cleqh  2873  nfcii  2904  nfcri  2907  bnj596  31154  bnj1146  31200  bnj1379  31239  bnj1464  31252  bnj1468  31254  bnj605  31315  bnj607  31324  bnj916  31341  bnj964  31351  bnj981  31358  bnj983  31359  bnj1014  31368  bnj1123  31392  bnj1373  31436  bnj1417  31447  bnj1445  31450  bnj1463  31461  bnj1497  31466  bj-cbv3hv2  33064  bj-equsalhv  33080  bj-nfs1v  33095  bj-nfsab1  33108  wl-nfalv  33647  nfequid-o  34718  nfa1-o  34723  2sb5ndVD  39668  2sb5ndALT  39690
 Copyright terms: Public domain W3C validator