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

Theorem nfn 1811
 Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfn.1
Assertion
Ref Expression
nfn

Proof of Theorem nfn
StepHypRef Expression
1 nfn.1 . . . 4
21a1i 11 . . 3
32nfnd 1809 . 2
43trud 1332 1
 Colors of variables: wff set class Syntax hints:   wn 3   wtru 1325  wnf 1553 This theorem is referenced by:  nfnan  1847  nfanOLD  1848  nfor  1858  nfexOLD  1866  dvelimhw  1876  19.32  1896  spimeOLD  1959  cbvex  1983  equsexOLD  2003  nfnae  2044  ax15  2101  mo  2302  euor  2307  euor2  2348  2mo  2358  nfne  2689  nfnel  2694  nfrex  2753  cbvrexf  2919  spcimegf  3022  spcegf  3024  cbvrexcsf  3304  nfdif  3460  nfpo  4500  nffr  4548  rexxpf  5012  0neqopab  6111  boxcutc  7097  nfoi  7475  stoweidlem34  27750  stoweidlem55  27771  stoweidlem59  27775  r19.32  27912  a9e2ndeqALT  28980  bnj1476  29155  bnj1388  29339  bnj1398  29340  bnj1445  29350  bnj1449  29354  nfexwAUX7  29388  nfnaewAUX7  29419  nfnaew2AUX7  29422  nfeqfNEW7  29423  equsexNEW7  29427  exdistrfNEW7  29442  spimeNEW7  29446  cbvexwAUX7  29457  nfnaew3AUX7  29463  ax15NEW7  29473  nfsb2NEW7  29498  sbco2wAUX7  29522  sb8iwAUX7  29526  sb8ewAUX7  29531  ax7w15lemxAUX7  29603  ax7w15lemAUX7  29604  ax7w14lemAUX7  29606  nfexOLD7  29625  nfnaeOLD7  29648  cbvexOLD7  29663  dvelimfOLD7  29664  nfsb4tw2AUXOLD7  29683  dvelimdfOLD7  29688  sbco2OLD7  29689  sbcomOLD7  29692  sb8eOLD7  29694  sb9iOLD7  29695  cdlemefs32sn1aw  31148 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-tru 1328  df-ex 1551  df-nf 1554
 Copyright terms: Public domain W3C validator