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

Theorem sbie 2123
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 2080 . . 3  |-  [ y  /  x ] x  =  y
2 sbie.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32sbimi 1717 . . 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 2094 . . 3  |-  ( [ y  /  x ] ps 
<->  ps )
76sblbis 2119 . 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 1599   [wsb 1711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712
This theorem is referenced by:  sbied  2125  equsb3lem  2158  elsb3  2161  elsb4  2162  cbveu  2318  mo4f  2338  2mos  2385  bm1.1OLD  2451  eqsb3lem  2586  clelsb3  2588  cbvab  2608  cbvabOLD  2609  cbvralf  3082  cbvreu  3086  sbralie  3101  cbvrab  3111  reu2  3291  nfcdeq  3328  sbcco2  3355  sbcie2g  3365  sbcralt  3412  sbcrexgOLD  3417  sbcreu  3418  sbcreugOLD  3419  cbvralcsf  3467  cbvreucsf  3469  cbvrabcsf  3470  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  sbss  3937  sbcbr123  4498  sbcbrgOLD  4499  cbvopab1  4517  cbvmpt  4537  cbviota  5554  cbvriota  6253  tfis2f  6668  tfinds  6672  nd1  8958  nd2  8959  clelsb3f  27055  rmo4fOLD  27071  rmo4f  27072  funcnv4mpt  27184  nn0min  27279  ballotlemodife  28076  setinds2f  28788  wfis2fg  28868  frins2fg  28904  prtlem5  30201  bnj1321  33162  bj-clelsb3  33505  bj-sbeqALT  33548
  Copyright terms: Public domain W3C validator