Theorem nf5i 2141

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

Step	Hyp	Ref	Expression
1		nf5-1 2140	. 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2		nf5i.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1798	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2136

This theorem depends on definitions:  df-bi 206  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnaew  2144  nfnaewOLD  2145  nfe1  2146  sbh  2264  nf5di  2281  19.9h  2282  19.21h  2283  19.23h  2284  exlimih  2285  exlimdh  2286  equsalhw  2287  equsexhv  2288  hban  2296  hb3an  2297  nfal  2316  hbex  2318  nfsbv  2323  hbsbwOLD  2325  cbv3hv  2336  dvelimhw  2341  cbv3h  2402  equsalh  2418  equsexh  2419  nfae  2431  axc16i  2434  dvelimh  2448  nfs1  2490  hbsb  2527  sb7h  2529  nfsab  2726  nfsabg  2727  cleqh  2860  nfcii  2888  nfcriOLDOLDOLD  2898  nfralw  3290  bnj596  33025  bnj1146  33070  bnj1379  33109  bnj1464  33123  bnj1468  33125  bnj605  33186  bnj607  33195  bnj916  33212  bnj964  33222  bnj981  33229  bnj983  33230  bnj1014  33240  bnj1123  33265  bnj1373  33309  bnj1417  33320  bnj1445  33323  bnj1463  33334  bnj1497  33339  bj-cbv3hv2  35073  bj-equsalhv  35084  bj-nfs1v  35091  bj-nfsab1  35094  bj-gabima  35223  wl-nfalv  35797  nfequid-o  37185  nfa1-o  37190  2sb5ndVD  42859  2sb5ndALT  42881