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

Theorem sbie 1991
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 1544 . . 3  |-  F/ x  T.
2 sbie.1 . . . 4  |-  F/ x ps
32a1i 10 . . 3  |-  (  T. 
->  F/ x ps )
4 sbie.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
54a1i 10 . . 3  |-  (  T. 
->  ( x  =  y  ->  ( ph  <->  ps )
) )
61, 3, 5sbied 1989 . 2  |-  (  T. 
->  ( [ y  /  x ] ph  <->  ps )
)
76trud 1314 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    T. wtru 1307   F/wnf 1534   [wsb 1638
This theorem is referenced by:  equsb3lem  2053  elsb3  2055  elsb4  2056  cbveu  2176  mo4f  2188  2mos  2235  bm1.1  2281  eqsb3lem  2396  clelsb3  2398  cbvab  2414  cbvralf  2771  cbvreu  2775  sbralie  2790  cbvrab  2799  reu2  2966  nfcdeq  3001  sbcco2  3027  sbcie2g  3037  sbcel2gv  3064  sbcralt  3076  sbcralg  3078  sbcrexg  3079  sbcreug  3080  sbcel12g  3109  sbceqg  3110  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  sbss  3576  sbcbrg  4088  cbvopab1  4105  cbvmpt  4126  tfis2f  4662  tfisi  4665  tfinds  4666  cbviota  5240  cbvriota  6331  nd1  8225  nd2  8226  ballotlemodife  23072  clelsb3f  23158  rmo4fOLD  23195  rmo4f  23196  cbvmptf  23235  funcnv4mpt  23252  setinds2f  24206  wfis2fg  24282  frins2fg  24318  prtlem5  26825  bnj1321  29373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639
  Copyright terms: Public domain W3C validator