Theorem nf5i 2144

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 2143	. 2 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
2		nf5i.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpg 1792	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1529  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2139

This theorem depends on definitions:  df-bi 209  df-ex 1775  df-nf 1779

This theorem is referenced by:  nfnaew  2147  nfe1  2148  sbh  2266  nf5di  2287  19.9h  2288  19.21h  2289  19.23h  2290  exlimih  2291  exlimdh  2292  equsalhw  2293  equsexhv  2294  hban  2302  hb3an  2303  nfal  2336  hbex  2338  hbsbw  2345  cbv3hv  2354  dvelimhw  2360  cbv3h  2418  equsalh  2436  equsexh  2437  nfae  2449  axc16i  2452  dvelimh  2466  nfs1  2521  hbsb  2561  sb7h  2563  nfsab1OLD  2807  nfsab  2810  nfsabg  2811  cleqh  2934  nfcii  2963  nfcri  2969  bnj596  32010  bnj1146  32056  bnj1379  32095  bnj1464  32109  bnj1468  32111  bnj605  32172  bnj607  32181  bnj916  32198  bnj964  32208  bnj981  32215  bnj983  32216  bnj1014  32226  bnj1123  32251  bnj1373  32295  bnj1417  32306  bnj1445  32309  bnj1463  32320  bnj1497  32325  bj-cbv3hv2  34110  bj-equsalhv  34121  bj-nfs1v  34128  bj-nfsab1  34131  wl-nfalv  34757  nfequid-o  36038  nfa1-o  36043  2sb5ndVD  41235  2sb5ndALT  41257