New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfbi Unicode version

Theorem nfbi 1834
 Description: If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
nf.1
nf.2
Assertion
Ref Expression
nfbi

Proof of Theorem nfbi
StepHypRef Expression
1 nf.1 . . . 4
21a1i 10 . . 3
3 nf.2 . . . 4
43a1i 10 . . 3
52, 4nfbid 1832 . 2
65trud 1323 1
 Colors of variables: wff setvar class Syntax hints:   wb 176   wtru 1316  wnf 1544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545 This theorem is referenced by:  euf  2210  sb8eu  2222  bm1.1  2338  abbi  2463  nfeq  2496  cleqf  2513  sbhypf  2904  ceqsexg  2970  elabgt  2982  elabgf  2983  cbviota  4344  sb8iota  4346  copsex2t  4608  copsex2g  4609  opelopabsb  4697  opeliunxp2  4822  ralxpf  4827  nfiso  5487
 Copyright terms: Public domain W3C validator