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

Theorem nfal 2151
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 2063 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2034 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2022 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1479  wnf 1706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-11 2032  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-ex 1703  df-nf 1708
This theorem is referenced by:  nfex  2152  nfnf  2156  nfaldOLD  2164  nfa2OLD  2166  aaan  2168  cbv3v  2170  pm11.53  2177  19.12vv  2178  cbv3  2263  cbval2  2277  nfsb4t  2387  euf  2476  mo2  2477  2eu3  2553  bm1.1  2605  nfnfc1  2765  nfnfc  2771  nfnfcALT  2772  sbcnestgf  3986  dfnfc2OLD  4446  nfdisj  4623  nfdisj1  4624  axrep1  4763  axrep2  4764  axrep3  4765  axrep4  4766  nffr  5078  zfcndrep  9421  zfcndinf  9425  mreexexd  16289  mreexexdOLD  16290  mptelee  25756  mo5f  29296  19.12b  31681  bj-cbv2v  32707  bj-cbval2v  32712  bj-axrep1  32763  bj-axrep2  32764  bj-axrep3  32765  bj-axrep4  32766  ax11-pm2  32798  bj-nfnfc  32828  wl-sb8t  33304  wl-mo2tf  33324  wl-eutf  33326  wl-mo2t  33328  wl-mo3t  33329  wl-sb8eut  33330  mpt2bi123f  33942  pm11.57  38409  pm11.59  38411  nfsetrecs  42198
  Copyright terms: Public domain W3C validator