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

Theorem nfnd 1760
 Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypothesis
Ref Expression
nfnd.1
Assertion
Ref Expression
nfnd

Proof of Theorem nfnd
StepHypRef Expression
1 nfnd.1 . 2
2 nfnf1 1757 . . 3
3 ax6o 1723 . . . . 5
43con1i 121 . . . 4
5 df-nf 1532 . . . . 5
6 con3 126 . . . . . 6
76al2imi 1548 . . . . 5
85, 7sylbi 187 . . . 4
94, 8syl5 28 . . 3
102, 9nfd 1746 . 2
111, 10syl 15 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4  wal 1527  wnf 1531 This theorem is referenced by:  nfbid  1762  nfand  1763  nfn  1765  nfexd  1776  19.9t  1782  nfexd2  1913  cbvexd  1949  nfned  2541  nfneld  2542  nfrexd  2595  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregndlem2  8225  axregnd  8226  distel  24160 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-11 1715 This theorem depends on definitions:  df-bi 177  df-nf 1532
 Copyright terms: Public domain W3C validator