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

Theorem nfal 1952
Description: If  x is not free in  ph, it is not free in  A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfal.1  |-  F/ x ph
Assertion
Ref Expression
nfal  |-  F/ x A. y ph

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4  |-  F/ x ph
21nfri 1879 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1849 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1628 1  |-  F/ x A. y ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1396   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-11 1847  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  nfnf  1954  nfald  1956  nfa2  1958  aaan  1980  pm11.53  1988  19.12vv  1991  cbv3  2020  cbval2  2032  nfsb4t  2132  euf  2294  mo2  2295  2eu3  2376  bm1.1  2437  bm1.1OLD  2438  nfnfc1  2619  nfnfc  2625  nfnfcALT  2626  nfeqOLD  2628  sbcnestgf  3834  dfnfc2  4253  nfdisj  4422  nfdisj1  4423  axrep1  4551  axrep2  4552  axrep3  4553  axrep4  4554  nffr  4842  zfcndrep  8981  zfcndinf  8985  mreexexd  15137  mptelee  24400  mo5f  27581  19.12b  29474  wl-sb8t  30240  wl-mo2t  30260  wl-mo3t  30261  wl-sb8eut  30262  mpt2bi123f  30811  pm11.57  31536  pm11.59  31538  bj-cbv3v  34689  bj-cbv2v  34696  bj-cbval2v  34703  bj-axrep1  34775  bj-axrep2  34776  bj-axrep3  34777  bj-axrep4  34778  ax11-pm2  34810  bj-nfnfc  34830
  Copyright terms: Public domain W3C validator