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

Theorem nfsb 2109
 Description: If is not free in , it is not free in when and are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfsb.1
Assertion
Ref Expression
nfsb
Distinct variable group:   ,
Allowed substitution hints:   (,,)

Proof of Theorem nfsb
StepHypRef Expression
1 a16nf 2051 . 2
2 nfsb.1 . . 3
32nfsb4 2081 . 2
41, 3pm2.61i 156 1
 Colors of variables: wff setvar class Syntax hints:  wal 1540  wnf 1544  wsb 1648 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649 This theorem is referenced by:  hbsb  2110  2sb5rf  2117  2sb6rf  2118  sb10f  2122  sb8eu  2222  2mo  2282  2eu6  2289  cbvab  2471  cbvralf  2829  cbvreu  2833  cbvralsv  2846  cbvrexsv  2847  cbvrab  2857  cbvreucsf  3200  cbvrabcsf  3201  cbviota  4344  sb8iota  4346  cbvopab1  4632  ralxpf  4827  cbvmpt  5676
 Copyright terms: Public domain W3C validator