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

Theorem nfald 1787
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 1757 . 2  |-  ( ph  ->  A. y F/ x ps )
4 nfnf1 1769 . . . 4  |-  F/ x F/ x ps
54nfal 1778 . . 3  |-  F/ x A. y F/ x ps
6 nfr 1753 . . . . 5  |-  ( F/ x ps  ->  ( ps  ->  A. x ps )
)
76al2imi 1551 . . . 4  |-  ( A. y F/ x ps  ->  ( A. y ps  ->  A. y A. x ps ) )
8 ax-7 1720 . . . 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 1758 . 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 1530   F/wnf 1534
This theorem is referenced by:  nfexd  1788  nfald2  1925  nfsb4t  2033  nfeqd  2446  axrepndlem1  8230  axrepndlem2  8231  axunnd  8234  axpowndlem2  8236  axpowndlem4  8238  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator