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

Theorem nfbi 1934
Description: If is not free in and , it is not free in . (Contributed by NM, 26-May-1993.) (Revised 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 11 . . 3
3 nf.2 . . . 4
43a1i 11 . . 3
52, 4nfbid 1933 . 2
65trud 1404 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184   wtru 1396  F/wnf 1616
This theorem is referenced by:  euf  2292  sb8eu  2318  sb8euOLD  2319  bm1.1  2440  bm1.1OLD  2441  cleqh  2572  abbiOLD  2589  nfeqOLD  2631  cleqfOLD  2647  sbhypf  3156  ceqsexg  3231  elabgt  3243  elabgf  3244  axrep1  4564  axrep3  4566  axrep4  4567  copsex2t  4739  copsex2g  4740  opelopabsb  4762  opeliunxp2  5146  ralxpf  5154  cbviota  5561  sb8iota  5563  fvopab5  5979  fmptco  6064  nfiso  6220  dfoprab4f  6858  xpf1o  7699  zfcndrep  9013  uzindOLD  10982  gsumcom2  17003  isfildlem  20358  cnextfvval  20565  mbfsup  22071  mbfinf  22072  fmptcof2  27502  subtr2  30133  mpt2bi123f  30571  fourierdlem31  31920  bnj1468  33904  bj-abbi  34361  bj-axrep1  34374  bj-axrep3  34376  bj-axrep4  34377
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-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator