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

Theorem nfal 2322
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 2193 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2171 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2146 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1541  wnf 1791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-10 2141  ax-11 2158  ax-12 2175
This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792
This theorem is referenced by:  nfex  2323  nfnf  2325  nfsbvOLD  2330  aaan  2333  cbval2v  2343  cbval2vOLD  2344  pm11.53  2347  19.12vv  2348  cbval2  2410  nfsb4t  2502  mof  2562  euf  2575  2eu3  2654  axextmo  2712  nfnfc1  2907  nfnfc  2916  nfabdwOLD  2928  sbcnestgfw  4333  sbcnestgf  4338  nfdisjw  5030  nfdisj  5031  nfdisj1  5032  axrep1  5180  axrep2  5182  axrep3  5183  axrep4  5184  nffr  5525  zfcndrep  10228  zfcndinf  10232  mreexexd  17151  mptelee  26986  mo5f  30556  iinabrex  30627  19.12b  33496  bj-cbv2v  34717  ax11-pm2  34756  wl-sb8t  35444  wl-mo2tf  35463  wl-eutf  35465  wl-mo2t  35467  wl-mo3t  35468  wl-sb8eut  35469  mpobi123f  36057  pm11.57  41680  pm11.59  41682  ichnfimlem  44588  ichnfim  44589  nfsetrecs  46063
  Copyright terms: Public domain W3C validator