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

Theorem nfsb 2184
 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:   ,

Proof of Theorem nfsb
StepHypRef Expression
1 ax16nf 1944 . 2
2 nfsb.1 . . 3
32nfsb4 2131 . 2
41, 3pm2.61i 164 1
 Colors of variables: wff setvar class Syntax hints:  A.wal 1393  F/wnf 1616  [wsb 1739 This theorem is referenced by:  hbsb  2185  sb10f  2200  2sb8e  2211  sb8eu  2318  sb8euOLD  2319  2mo  2373  2moOLD  2374  2eu6OLD  2384  cbvabOLD  2599  cbvralf  3078  cbvreu  3082  cbvralsv  3095  cbvrexsv  3096  cbvrab  3107  cbvreucsf  3468  cbvrabcsf  3469  cbvopab1  4522  cbvmpt  4542  ralxpf  5154  cbviota  5561  sb8iota  5563  cbvriota  6267  dfoprab4f  6858  mo5f  27383  cbvmptf  27494  2sb5nd  33333  ax11-pm2  34409 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-11 1842  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740
 Copyright terms: Public domain W3C validator