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

Theorem nfal 2139
 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 2053 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2023 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2011 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1473  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701 This theorem is referenced by:  nfex  2140  nfnf  2144  nfaldOLD  2152  nfa2OLD  2154  aaan  2156  cbv3v  2158  pm11.53  2167  19.12vv  2168  cbv3  2253  cbvalv  2261  cbval2  2267  nfsb4t  2377  euf  2466  mo2  2467  2eu3  2543  bm1.1  2595  nfnfc1  2754  nfnfc  2760  nfnfcALT  2761  sbcnestgf  3947  dfnfc2OLD  4391  nfdisj  4565  nfdisj1  4566  axrep1  4700  axrep2  4701  axrep3  4702  axrep4  4703  nffr  5012  zfcndrep  9315  zfcndinf  9319  mreexexd  16131  mreexexdOLD  16132  mptelee  25575  mo5f  28708  19.12b  30951  bj-cbv2v  31919  bj-cbval2v  31924  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  ax11-pm2  32011  bj-nfnfc  32047  wl-sb8t  32512  wl-mo2tf  32532  wl-eutf  32534  wl-mo2t  32536  wl-mo3t  32537  wl-sb8eut  32538  mpt2bi123f  33141  pm11.57  37611  pm11.59  37613  nfsetrecs  42232
 Copyright terms: Public domain W3C validator