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

Theorem nfal 2317
Description: If 𝑥 is not free in 𝜑, then 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 2189 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2168 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2143 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1540  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787
This theorem is referenced by:  nfex  2318  nfnf  2320  nfsbvOLD  2325  aaanOLD  2329  cbval2v  2340  pm11.53  2343  19.12vv  2344  cbval2  2411  nfsb4t  2499  mof  2558  euf  2571  2eu3  2650  axextmo  2708  nfnfc1  2907  nfnfc  2916  nfabdwOLD  2928  sbcnestgfw  4417  sbcnestgf  4422  nfdisjw  5124  nfdisj  5125  nfdisj1  5126  axrep1  5285  axrep2  5287  axrep3  5288  axrep4  5289  nffr  5649  zfcndrep  10605  zfcndinf  10609  mreexexd  17588  mptelee  28133  mo5f  31707  iinabrex  31778  19.12b  34711  bj-cbv2v  35614  ax11-pm2  35652  wl-sb8t  36355  wl-mo2tf  36374  wl-eutf  36376  wl-mo2t  36378  wl-mo3t  36379  wl-sb8eut  36380  mpobi123f  36968  pm11.57  43081  pm11.59  43083  ichnfimlem  46066  ichnfim  46067  nfsetrecs  47633  pgind  47664
  Copyright terms: Public domain W3C validator