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

Theorem nfsb 2155
 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 ax16nf 1882 . 2
2 nfsb.1 . . 3
32nfsb4 2091 . 2
41, 3pm2.61i 164 1
 Colors of variables: wff setvar class Syntax hints:  wal 1368  wnf 1590  wsb 1702 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703 This theorem is referenced by:  hbsb  2156  2sb5rfOLD  2170  2sb6rfOLD  2171  sb10f  2175  2sb8e  2189  sb8eu  2301  sb8euOLD  2302  sb8euOLDOLD  2303  2mo  2369  2moOLD  2370  2moOLDOLD  2371  2eu6OLD  2381  cbvabOLD  2596  cbvralf  3047  cbvreu  3051  cbvralsv  3064  cbvrexsv  3065  cbvrab  3076  cbvreucsf  3432  cbvrabcsf  3433  cbvopab1  4473  cbvmpt  4493  ralxpf  5097  cbviota  5497  sb8iota  5499  cbvriota  6174  dfoprab4f  6745  mo5f  26047  cbvmptf  26149  2sb5nd  31624  ax11-pm2  32701
 Copyright terms: Public domain W3C validator