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

Theorem nfald 1951
 Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)
Hypotheses
Ref Expression
nfald.1
nfald.2
Assertion
Ref Expression
nfald

Proof of Theorem nfald
StepHypRef Expression
1 nfald.1 . . 3
2 nfald.2 . . 3
31, 2alrimi 1877 . 2
4 nfnf1 1899 . . . 4
54nfal 1947 . . 3
6 hba1 1896 . . . 4
7 sp 1859 . . . . 5
87nfrd 1875 . . . 4
96, 8hbald 1848 . . 3
105, 9nfd 1878 . 2
113, 10syl 16 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616 This theorem is referenced by:  nfexd  1952  dvelimhw  1955  nfald2  2073  nfeqd  2626  axrepndlem1  8988  axrepndlem2  8989  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  wl-mo2dnae  30019  wl-mo2t  30020 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854 This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator