MPE Home 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