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

Theorem sbie 2149
Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.)
Hypotheses
Ref Expression
sbie.1
sbie.2
Assertion
Ref Expression
sbie

Proof of Theorem sbie
StepHypRef Expression
1 equsb1 2107 . . 3
2 sbie.2 . . . 4
32sbimi 1745 . . 3
41, 3ax-mp 5 . 2
5 sbie.1 . . . 4
65sbf 2121 . . 3
76sblbis 2145 . 2
84, 7mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  F/wnf 1616  [wsb 1739
This theorem is referenced by:  sbied  2151  equsb3lem  2175  elsb3  2178  elsb4  2179  cbveu  2321  mo4f  2336  2mos  2375  bm1.1OLD  2441  eqsb3lem  2576  clelsb3  2578  cbvab  2598  cbvabOLD  2599  cbvralf  3078  cbvreu  3082  sbralie  3097  cbvrab  3107  reu2  3287  nfcdeq  3324  sbcco2  3351  sbcie2g  3361  sbcralt  3408  sbcrexgOLD  3413  sbcreu  3414  sbcreugOLD  3415  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  sbss  3939  sbcbr123  4503  sbcbrgOLD  4504  cbvopab1  4522  cbvmpt  4542  cbviota  5561  cbvriota  6267  tfis2f  6690  tfinds  6694  nd1  8983  nd2  8984  clelsb3f  27379  rmo4fOLD  27395  rmo4f  27396  funcnv4mpt  27512  nn0min  27611  ballotlemodife  28436  setinds2f  29211  wfis2fg  29291  frins2fg  29327  prtlem5  30597  bnj1321  34083  bj-clelsb3  34424  bj-sbeqALT  34467  frege70  37961  frege72  37963
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-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740
  Copyright terms: Public domain W3C validator