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

Theorem sbie 2098
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 2054 . . 3  |-  [ y  /  x ] x  =  y
2 sbie.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32sbimi 1705 . . 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 2068 . . 3  |-  ( [ y  /  x ] ps 
<->  ps )
76sblbis 2094 . 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 1592   [wsb 1699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791  ax-13 1942
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700
This theorem is referenced by:  sbied  2100  equsb3lem  2138  elsb3  2141  elsb4  2142  cbveu  2297  mo4f  2311  2mos  2357  bm1.1  2418  eqsb3lem  2533  clelsb3  2535  cbvab  2551  cbvralf  2931  cbvreu  2935  sbralie  2950  cbvrab  2960  reu2  3136  nfcdeq  3172  sbcco2  3198  sbcie2g  3208  sbcralt  3255  sbcrexgOLD  3260  sbcreu  3261  sbcreugOLD  3262  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  sbcel12  3663  sbcel12gOLD  3664  sbceqg  3665  sbss  3777  sbcbr123  4331  sbcbrgOLD  4332  cbvopab1  4350  cbvmpt  4370  cbviota  5374  cbvriota  6050  tfis2f  6455  tfinds  6459  nd1  8739  nd2  8740  clelsb3f  25687  rmo4fOLD  25704  rmo4f  25705  funcnv4mpt  25813  nn0min  25913  ballotlemodife  26728  setinds2f  27439  wfis2fg  27519  frins2fg  27555  prtlem5  28846  bnj1321  31741  bj-clelsb3  31992  bj-sbeqALT  32017
  Copyright terms: Public domain W3C validator