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

Theorem sbie 2200
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 2158 . . 3  |-  [ y  /  x ] x  =  y
2 sbie.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32sbimi 1792 . . 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 2172 . . 3  |-  ( [ y  /  x ] ps 
<->  ps )
76sblbis 2196 . 2  |-  ( [ y  /  x ]
( ph  <->  ps )  <->  ( [
y  /  x ] ph 
<->  ps ) )
84, 7mpbi 211 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   F/wnf 1663   [wsb 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-12 1904  ax-13 2052
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787
This theorem is referenced by:  sbied  2201  equsb3lem  2224  elsb3  2227  elsb4  2228  cbveu  2299  mo4f  2310  2mos  2347  bm1.1OLD  2404  eqsb3lem  2539  clelsb3  2541  cbvab  2561  cbvabOLD  2562  cbvralf  3047  cbvreu  3051  sbralie  3066  cbvrab  3076  reu2  3256  nfcdeq  3293  sbcco2  3320  sbcie2g  3330  sbcralt  3369  sbcreu  3373  cbvralcsf  3424  cbvreucsf  3426  cbvrabcsf  3427  sbcel12  3797  sbceqg  3798  sbss  3904  sbcbr123  4469  cbvopab1  4488  cbvmpt  4509  wfis2fg  5428  cbviota  5562  cbvriota  6269  tfis2f  6688  tfinds  6692  nd1  9008  nd2  9009  clelsb3f  28092  rmo4fOLD  28108  rmo4f  28109  funcnv4mpt  28254  nn0min  28371  ballotlemodife  29319  bnj1321  29825  setinds2f  30413  frins2fg  30473  bj-clelsb3  31409  bj-sbeqALT  31453  prtlem5  32340  sbcrexgOLD  35541  sbcel12gOLD  36757
  Copyright terms: Public domain W3C validator