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

Theorem sbie 2100
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  |-  F/ x ps
sbie.2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
sbie  |-  ( [ y  /  x ] ph 
<->  ps )

Proof of Theorem sbie
StepHypRef Expression
1 equsb1 2057 . . 3  |-  [ y  /  x ] x  =  y
2 sbie.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32sbimi 1706 . . 3  |-  ( [ y  /  x ]
x  =  y  ->  [ y  /  x ] ( ph  <->  ps )
)
41, 3ax-mp 5 . 2  |-  [ y  /  x ] (
ph 
<->  ps )
5 sbie.1 . . . 4  |-  F/ x ps
65sbf 2071 . . 3  |-  ( [ y  /  x ] ps 
<->  ps )
76sblbis 2096 . 2  |-  ( [ y  /  x ]
( ph  <->  ps )  <->  ( [
y  /  x ] ph 
<->  ps ) )
84, 7mpbi 208 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1589   [wsb 1700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701
This theorem is referenced by:  sbied  2102  equsb3lem  2136  elsb3  2139  elsb4  2140  cbveu  2296  mo4f  2316  2mos  2363  bm1.1OLD  2428  eqsb3lem  2546  clelsb3  2548  cbvab  2564  cbvralf  2944  cbvreu  2948  sbralie  2963  cbvrab  2973  reu2  3150  nfcdeq  3186  sbcco2  3213  sbcie2g  3223  sbcralt  3270  sbcrexgOLD  3275  sbcreu  3276  sbcreugOLD  3277  cbvralcsf  3322  cbvreucsf  3324  cbvrabcsf  3325  sbcel12  3678  sbcel12gOLD  3679  sbceqg  3680  sbss  3792  sbcbr123  4346  sbcbrgOLD  4347  cbvopab1  4365  cbvmpt  4385  cbviota  5389  cbvriota  6065  tfis2f  6469  tfinds  6473  nd1  8754  nd2  8755  clelsb3f  25867  rmo4fOLD  25883  rmo4f  25884  funcnv4mpt  25992  nn0min  26093  ballotlemodife  26883  setinds2f  27595  wfis2fg  27675  frins2fg  27711  prtlem5  29004  bnj1321  32021  bj-clelsb3  32362  bj-sbeqALT  32405
  Copyright terms: Public domain W3C validator