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

Theorem nfal 1873
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 1808 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1782 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1596 1  |-  F/ x A. y ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1367   F/wnf 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-11 1780  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590
This theorem is referenced by:  nfnf  1875  nfald  1877  nfa2  1879  aaan  1903  pm11.53  1912  19.12vv  1917  cbv3  1959  cbv2  1967  cbval2  1975  nfsb4t  2080  euf  2263  eufOLD  2264  mo2  2265  moOLD  2305  2moOLDOLD  2362  2eu3  2367  bm1.1  2427  bm1.1OLD  2428  nfnfc1  2582  nfnfc  2585  nfeq  2586  sbcnestgf  3691  dfnfc2  4109  nfdisj  4274  nfdisj1  4275  axrep1  4404  axrep2  4405  axrep3  4406  axrep4  4407  nffr  4694  zfcndrep  8781  zfcndinf  8785  mreexexd  14586  mptelee  23141  mo5f  25868  19.12b  27615  wl-sb8t  28376  wl-mo2t  28396  wl-mo3t  28397  wl-sb8eut  28398  mpt2bi123f  28975  pm11.57  29642  pm11.59  29644  bj-cbv3v  32224  bj-cbv2v  32231  bj-cbval2v  32238  bj-axrep1  32309  bj-axrep2  32310  bj-axrep3  32311  bj-axrep4  32312  ax11-pm2  32344  bj-nfnfc  32364
  Copyright terms: Public domain W3C validator