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

Theorem nfal 1778
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
nf.1  |-  F/ x ph
Assertion
Ref Expression
nfal  |-  F/ x A. y ph

Proof of Theorem nfal
StepHypRef Expression
1 nf.1 . . . 4  |-  F/ x ph
21nfri 1754 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1722 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1541 1  |-  F/ x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfex  1779  nfnf  1780  nfald  1787  nfa2  1789  aaan  1837  pm11.53  1846  19.12vv  1851  cbval2  1957  sb8  2045  euf  2162  mo  2178  2mo  2234  2eu3  2238  bm1.1  2281  nfnfc1  2435  nfnfc  2438  nfeq  2439  sbcnestgf  3141  dfnfc2  3861  nfdisj  4021  nfdisj1  4022  axrep1  4148  axrep2  4149  axrep3  4150  axrep4  4151  nffr  4383  zfcndrep  8252  zfcndinf  8256  mreexexd  13566  mo5f  23159  19.12b  24229  mptelee  24595  pm11.53g  25067  pm11.57  27691  pm11.59  27693
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-7 1720  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator