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

Theorem hban 1851
 Description: If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
hb.1
hb.2
Assertion
Ref Expression
hban

Proof of Theorem hban
StepHypRef Expression
1 hb.1 . . . 4
21nfi 1561 . . 3
3 hb.2 . . . 4
43nfi 1561 . . 3
52, 4nfan 1847 . 2
65nfri 1779 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360  wal 1550 This theorem is referenced by:  hb3anOLD  1854  dvelimvOLD  2029  dvelimhOLD  2073  dvelimALT  2212  dvelimf-o  2259  ax11indalem  2276  ax11inda2ALT  2277  cleqh  2535  hbimpg  28715  hbimpgVD  29090  bnj982  29223  bnj1351  29272  bnj1352  29273  bnj1441  29286  dvelimvNEW7  29536  dvelimhvAUX7  29566  dvelimALTNEW7  29710  dvelimhOLD7  29787 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
 Copyright terms: Public domain W3C validator