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

Theorem nfal 2316
 Description: If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfal.1 𝑥𝜑
Assertion
Ref Expression
nfal 𝑥𝑦𝜑

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4 𝑥𝜑
21nf5ri 2218 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2191 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2178 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1628  Ⅎwnf 1855 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-10 2173  ax-11 2189  ax-12 2202 This theorem depends on definitions:  df-bi 197  df-ex 1852  df-nf 1857 This theorem is referenced by:  nfex  2317  nfnf  2321  nfaldOLD  2327  nfa2OLD  2329  aaan  2330  cbv3v  2332  pm11.53  2340  19.12vv  2341  cbv3  2425  cbval2  2437  nfsb4t  2535  euf  2625  mo2  2626  2eu3  2703  bm1.1  2755  nfnfc1  2915  nfnfc  2922  nfnfcALT  2923  sbcnestgf  4137  nfdisj  4764  nfdisj1  4765  axrep1  4903  axrep2  4904  axrep3  4905  axrep4  4906  nffr  5223  zfcndrep  9637  zfcndinf  9641  mreexexd  16515  mptelee  25995  mo5f  29658  19.12b  32037  bj-cbv2v  33062  bj-cbval2v  33067  bj-axrep1  33118  bj-axrep2  33119  bj-axrep3  33120  bj-axrep4  33121  ax11-pm2  33152  wl-sb8t  33661  wl-mo2tf  33680  wl-eutf  33682  wl-mo2t  33684  wl-mo3t  33685  wl-sb8eut  33686  mpt2bi123f  34296  pm11.57  39108  pm11.59  39110  nfsetrecs  42951
 Copyright terms: Public domain W3C validator