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

Theorem nfald 1867
Description: If  x is not free in  ph, it is not free in  A. y ph. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)
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 1777 . 2  |-  ( ph  ->  A. y F/ x ps )
4 nfnf1 1804 . . . 4  |-  F/ x F/ x ps
54nfal 1860 . . 3  |-  F/ x A. y F/ x ps
6 hba1 1800 . . . 4  |-  ( A. y F/ x ps  ->  A. y A. y F/ x ps )
7 sp 1759 . . . . 5  |-  ( A. y F/ x ps  ->  F/ x ps )
87nfrd 1775 . . . 4  |-  ( A. y F/ x ps  ->  ( ps  ->  A. x ps ) )
96, 8hbald 1751 . . 3  |-  ( A. y F/ x ps  ->  ( A. y ps  ->  A. x A. y ps ) )
105, 9nfd 1778 . 2  |-  ( A. y F/ x ps  ->  F/ x A. y ps )
113, 10syl 16 1  |-  ( ph  ->  F/ x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546   F/wnf 1550
This theorem is referenced by:  nfexd  1869  dvelimhw  1872  ax12olem4  1975  dvelimh  2017  nfald2  2039  nfsb4t  2137  nfeqd  2562  axrepndlem1  8431  axrepndlem2  8432  axunnd  8435  axpowndlem2  8437  axpowndlem4  8439  axregndlem2  8442  axinfndlem1  8444  axinfnd  8445  axacndlem4  8449  axacndlem5  8450  axacnd  8451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator