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

Theorem nfal 2191
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 2103 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2076 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2064 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1521  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfex  2192  nfnf  2196  nfaldOLD  2202  nfa2OLD  2204  aaan  2206  cbv3v  2208  pm11.53  2215  19.12vv  2216  cbv3  2301  cbval2  2315  nfsb4t  2417  euf  2506  mo2  2507  2eu3  2584  bm1.1  2636  nfnfc1  2796  nfnfc  2803  nfnfcALT  2804  sbcnestgf  4028  dfnfc2OLD  4487  nfdisj  4664  nfdisj1  4665  axrep1  4805  axrep2  4806  axrep3  4807  axrep4  4808  nffr  5117  zfcndrep  9474  zfcndinf  9478  mreexexd  16355  mreexexdOLD  16356  mptelee  25820  mo5f  29452  19.12b  31831  bj-cbv2v  32857  bj-cbval2v  32862  bj-axrep1  32913  bj-axrep2  32914  bj-axrep3  32915  bj-axrep4  32916  ax11-pm2  32948  bj-nfnfc  32978  wl-sb8t  33463  wl-mo2tf  33483  wl-eutf  33485  wl-mo2t  33487  wl-mo3t  33488  wl-sb8eut  33489  mpt2bi123f  34101  pm11.57  38906  pm11.59  38908  nfsetrecs  42758
  Copyright terms: Public domain W3C validator