ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfbi Structured version   Unicode version

Theorem nfbi 1478
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
nfbi.1  F/
nfbi.2  F/
Assertion
Ref Expression
nfbi  F/

Proof of Theorem nfbi
StepHypRef Expression
1 nfbi.1 . . . 4  F/
21a1i 9 . . 3  F/
3 nfbi.2 . . . 4  F/
43a1i 9 . . 3  F/
52, 4nfbid 1477 . 2  F/
65trud 1251 1  F/
Colors of variables: wff set class
Syntax hints:   wb 98   wtru 1243   F/wnf 1346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-ial 1424  ax-i5r 1425
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347
This theorem is referenced by:  sb8eu  1910  nfeuv  1915  bm1.1  2022  abbi  2148  nfeq  2182  cleqf  2198  sbhypf  2597  ceqsexg  2666  elabgt  2678  elabgf  2679  copsex2t  3973  copsex2g  3974  opelopabsb  3988  opeliunxp2  4419  ralxpf  4425  rexxpf  4426  cbviota  4815  sb8iota  4817  fmptco  5273  nfiso  5389  dfoprab4f  5761  bdsepnfALT  9277  strcollnfALT  9370
  Copyright terms: Public domain W3C validator