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

Theorem sbf 2121
Description: Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
Hypothesis
Ref Expression
sbf.1
Assertion
Ref Expression
sbf

Proof of Theorem sbf
StepHypRef Expression
1 sbf.1 . 2
2 sbft 2120 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  F/wnf 1616  [wsb 1739
This theorem is referenced by:  sbh  2122  sbf2  2123  nfs1f  2124  sb6x  2125  sbequ5  2128  sbequ6  2129  sbrim  2137  sblim  2138  sbrbif  2147  sbie  2149  sbieOLD  2150  sbid2  2155  equsb3  2176  sbcom4  2190  sbabel  2650  sbabelOLD  2651  nfcdeq  3324  mo5f  27383  iuninc  27428  suppss2f  27477  fmptdF  27495  disjdsct  27521  esumpfinvalf  28082  measiuns  28188  ballotlemodife  28436  wl-equsb3  30004  ellimcabssub0  31623  bj-sbf3  34410  bj-sbf4  34411  frege70  37961
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