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

Theorem sbie 2071
Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.)
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 nftru 1560 . . 3  |-  F/ x  T.
2 sbie.1 . . . 4  |-  F/ x ps
32a1i 11 . . 3  |-  (  T. 
->  F/ x ps )
4 sbie.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
54a1i 11 . . 3  |-  (  T. 
->  ( x  =  y  ->  ( ph  <->  ps )
) )
61, 3, 5sbied 2069 . 2  |-  (  T. 
->  ( [ y  /  x ] ph  <->  ps )
)
76trud 1329 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    T. wtru 1322   F/wnf 1550   [wsb 1655
This theorem is referenced by:  equsb3lem  2134  elsb3  2136  elsb4  2137  cbveu  2258  mo4f  2270  2mos  2317  bm1.1  2372  eqsb3lem  2487  clelsb3  2489  cbvab  2505  cbvralf  2869  cbvreu  2873  sbralie  2888  cbvrab  2897  reu2  3065  nfcdeq  3101  sbcco2  3127  sbcie2g  3137  sbcralt  3176  sbcralg  3178  sbcrexg  3179  sbcreug  3180  sbcel12g  3209  sbceqg  3210  cbvralcsf  3254  cbvreucsf  3256  cbvrabcsf  3257  sbss  3680  sbcbrg  4202  cbvopab1  4219  cbvmpt  4240  tfis2f  4775  tfinds  4779  cbviota  5363  cbvriota  6496  nd1  8395  nd2  8396  clelsb3f  23815  rmo4fOLD  23827  rmo4f  23828  funcnv4mpt  23926  ballotlemodife  24534  setinds2f  25159  wfis2fg  25235  frins2fg  25271  prtlem5  26396  bnj1321  28734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656
  Copyright terms: Public domain W3C validator