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

Theorem nfs1v 2181
Description: is not free in when and are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfs1v
Distinct variable group:   ,

Proof of Theorem nfs1v
StepHypRef Expression
1 hbs1 2180 . 2
21nfi 1623 1
Colors of variables: wff setvar class
Syntax hints:  F/wnf 1616  [wsb 1739
This theorem is referenced by:  mo3  2323  mo3OLD  2324  eu1  2327  2mo  2373  2moOLD  2374  2eu6  2383  2eu6OLD  2384  clelabOLD  2602  cbvralf  3078  cbvralsv  3095  cbvrexsv  3096  cbvrab  3107  sbhypf  3156  mob2  3279  reu2  3287  reu2eqd  3296  sbcralt  3408  sbcrexgOLD  3413  sbcreu  3414  sbcreugOLD  3415  cbvreucsf  3468  cbvrabcsf  3469  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  csbif  3991  csbifgOLD  3992  rabasiun  4334  cbvopab1  4522  cbvopab1s  4524  cbvmpt  4542  opelopabsb  4762  csbopab  4784  csbopabgALT  4785  opeliunxp  5056  ralxpf  5154  cbviota  5561  csbiota  5585  csbiotagOLD  5586  isarep1  5672  cbvriota  6267  csbriota  6269  onminex  6642  tfis  6689  findes  6730  abrexex2g  6777  abrexex2  6781  dfoprab4f  6858  axrepndlem1  8988  axrepndlem2  8989  uzind4s  11170  mo5f  27383  cbvmptf  27494  esumcvg  28092  wl-lem-moexsb  30017  wl-mo3t  30021  sbcalf  30517  sbcexf  30518  opeliun2xp  32922  2sb5nd  33333  2sb5ndALT  33732
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  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