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

Theorem nfal 1766
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 1742 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1710 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1538 1  |-  F/ x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfex  1767  nfnf  1768  nfald  1775  nfa2  1777  aaan  1825  pm11.53  1834  19.12vv  1839  cbval2  1944  sb8  2032  euf  2149  mo  2165  2mo  2221  2eu3  2225  bm1.1  2268  nfnfc1  2422  nfnfc  2425  nfeq  2426  sbcnestgf  3128  dfnfc2  3845  nfdisj  4005  nfdisj1  4006  axrep1  4132  axrep2  4133  axrep3  4134  axrep4  4135  nffr  4367  zfcndrep  8236  zfcndinf  8240  mreexexd  13550  mo5f  23143  19.12b  24158  mptelee  24523  pm11.53g  24964  pm11.57  27588  pm11.59  27590
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-7 1708  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator