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

Theorem nfal 2138
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 2052 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2022 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2010 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1472  wnf 1698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-ex 1695  df-nf 1700
This theorem is referenced by:  nfex  2139  nfnf  2143  nfaldOLD  2151  nfa2OLD  2153  aaan  2155  cbv3v  2157  pm11.53  2166  19.12vv  2167  cbv3  2252  cbvalv  2260  cbval2  2266  nfsb4t  2376  euf  2465  mo2  2466  2eu3  2542  bm1.1  2594  nfnfc1  2753  nfnfc  2759  nfnfcALT  2760  sbcnestgf  3946  dfnfc2OLD  4385  nfdisj  4559  nfdisj1  4560  axrep1  4694  axrep2  4695  axrep3  4696  axrep4  4697  nffr  5001  zfcndrep  9292  zfcndinf  9296  mreexexd  16079  mreexexdOLD  16080  mptelee  25520  mo5f  28501  19.12b  30744  bj-cbv2v  31712  bj-cbval2v  31717  bj-axrep1  31769  bj-axrep2  31770  bj-axrep3  31771  bj-axrep4  31772  ax11-pm2  31804  bj-nfnfc  31830  wl-sb8t  32295  wl-mo2tf  32315  wl-eutf  32317  wl-mo2t  32319  wl-mo3t  32320  wl-sb8eut  32321  mpt2bi123f  32924  pm11.57  37394  pm11.59  37396
  Copyright terms: Public domain W3C validator