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

Theorem nfal 1864
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 1778 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1751 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1560 1  |-  F/ x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1549   F/wnf 1553
This theorem is referenced by:  nfexOLD  1866  nfnf  1867  nfnfOLD  1868  nfald  1871  nfaldOLD  1872  nfa2  1874  aaan  1906  pm11.53  1916  19.12vv  1921  cbv3  1971  cbv2  1980  cbval2  1989  cbval2OLD  1990  nfsb4t  2127  euf  2287  mo  2303  2mo  2359  2eu3  2363  bm1.1  2421  nfnfc1  2575  nfnfc  2578  nfeq  2579  sbcnestgf  3298  dfnfc2  4033  nfdisj  4194  nfdisj1  4195  axrep1  4321  axrep2  4322  axrep3  4323  axrep4  4324  nffr  4556  zfcndrep  8489  zfcndinf  8493  mreexexd  13873  mo5f  23972  19.12b  25429  mptelee  25834  pm11.57  27565  pm11.59  27567
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-7 1749  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator