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

Theorem nfal 2049
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 1972 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1939 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1682 1  |-  F/ x A. y ph
Colors of variables: wff setvar class
Syntax hints:   A.wal 1450   F/wnf 1675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-11 1937  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676
This theorem is referenced by:  nfnf  2051  nfald  2053  nfa2  2055  aaan  2074  cbv3v  2078  pm11.53  2090  19.12vv  2091  cbv3  2121  cbval2  2133  nfsb4t  2238  euf  2327  mo2  2328  2eu3  2404  bm1.1  2456  nfnfc1  2615  nfnfc  2621  nfnfcALT  2622  sbcnestgf  3788  dfnfc2  4208  nfdisj  4378  nfdisj1  4379  axrep1  4509  axrep2  4510  axrep3  4511  axrep4  4512  nffr  4813  zfcndrep  9057  zfcndinf  9061  mreexexd  15632  mptelee  25004  mo5f  28199  19.12b  30519  bj-cbv2v  31399  bj-cbval2v  31404  bj-axrep1  31469  bj-axrep2  31470  bj-axrep3  31471  bj-axrep4  31472  ax11-pm2  31504  bj-nfnfc  31530  wl-sb8t  31950  wl-mo2tf  31970  wl-eutf  31972  wl-mo2t  31974  wl-mo3t  31975  wl-sb8eut  31976  mpt2bi123f  32470  pm11.57  36809  pm11.59  36811
  Copyright terms: Public domain W3C validator