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

Theorem nfald 1775
Description: If  x is not free in  ph, it is not free in  A. y ph. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfald.1  |-  F/ y
ph
nfald.2  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfald  |-  ( ph  ->  F/ x A. y ps )

Proof of Theorem nfald
StepHypRef Expression
1 nfald.1 . . 3  |-  F/ y
ph
2 nfald.2 . . 3  |-  ( ph  ->  F/ x ps )
31, 2alrimi 1745 . 2  |-  ( ph  ->  A. y F/ x ps )
4 nfnf1 1757 . . . 4  |-  F/ x F/ x ps
54nfal 1766 . . 3  |-  F/ x A. y F/ x ps
6 nfr 1741 . . . . 5  |-  ( F/ x ps  ->  ( ps  ->  A. x ps )
)
76al2imi 1548 . . . 4  |-  ( A. y F/ x ps  ->  ( A. y ps  ->  A. y A. x ps ) )
8 ax-7 1708 . . . 4  |-  ( A. y A. x ps  ->  A. x A. y ps )
97, 8syl6 29 . . 3  |-  ( A. y F/ x ps  ->  ( A. y ps  ->  A. x A. y ps ) )
105, 9nfd 1746 . 2  |-  ( A. y F/ x ps  ->  F/ x A. y ps )
113, 10syl 15 1  |-  ( ph  ->  F/ x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfexd  1776  nfald2  1912  nfsb4t  2020  nfeqd  2433  axrepndlem1  8214  axrepndlem2  8215  axunnd  8218  axpowndlem2  8220  axpowndlem4  8222  axregndlem2  8225  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234
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-6 1703  ax-7 1708  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator