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

Theorem sbie 2173
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 2131 . . 3  |-  [ y  /  x ] x  =  y
2 sbie.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32sbimi 1769 . . 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 2145 . . 3  |-  ( [ y  /  x ] ps 
<->  ps )
76sblbis 2169 . 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 1637   [wsb 1763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-12 1878  ax-13 2026
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1634  df-nf 1638  df-sb 1764
This theorem is referenced by:  sbied  2175  equsb3lem  2199  elsb3  2202  elsb4  2203  cbveu  2276  mo4f  2288  2mos  2326  bm1.1OLD  2386  eqsb3lem  2521  clelsb3  2523  cbvab  2543  cbvabOLD  2544  cbvralf  3027  cbvreu  3031  sbralie  3046  cbvrab  3056  reu2  3236  nfcdeq  3273  sbcco2  3300  sbcie2g  3310  sbcralt  3349  sbcreu  3353  cbvralcsf  3404  cbvreucsf  3406  cbvrabcsf  3407  sbcel12  3776  sbceqg  3777  sbss  3882  sbcbr123  4445  cbvopab1  4464  cbvmpt  4485  wfis2fg  5403  cbviota  5537  cbvriota  6249  tfis2f  6672  tfinds  6676  nd1  8993  nd2  8994  clelsb3f  27780  rmo4fOLD  27796  rmo4f  27797  funcnv4mpt  27941  nn0min  28049  ballotlemodife  28928  bnj1321  29397  setinds2f  29985  frins2fg  30045  bj-clelsb3  30975  bj-sbeqALT  31018  prtlem5  31859  sbcrexgOLD  35060  sbcel12gOLD  36315
  Copyright terms: Public domain W3C validator