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

Theorem nfald 1889
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 1816 . 2  |-  ( ph  ->  A. y F/ x ps )
4 nfnf1 1838 . . . 4  |-  F/ x F/ x ps
54nfal 1885 . . 3  |-  F/ x A. y F/ x ps
6 hba1 1835 . . . 4  |-  ( A. y F/ x ps  ->  A. y A. y F/ x ps )
7 sp 1799 . . . . 5  |-  ( A. y F/ x ps  ->  F/ x ps )
87nfrd 1814 . . . 4  |-  ( A. y F/ x ps  ->  ( ps  ->  A. x ps ) )
96, 8hbald 1788 . . 3  |-  ( A. y F/ x ps  ->  ( A. y ps  ->  A. x A. y ps ) )
105, 9nfd 1817 . 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 setvar class
Syntax hints:    -> wi 4   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfexd  1890  dvelimhw  1893  nfald2  2033  nfeqd  2623  axrepndlem1  8870  axrepndlem2  8871  axunnd  8874  axpowndlem2  8876  axpowndlem2OLD  8877  axpowndlem4  8880  axregndlem2  8883  axinfndlem1  8886  axinfnd  8887  axacndlem4  8891  axacndlem5  8892  axacnd  8893  wl-mo2dnae  28563  wl-mo2t  28564
  Copyright terms: Public domain W3C validator