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

Theorem sbie 2124
Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Revised by Wolf Lammen, 30-Apr-2018.)
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 sb1 1662 . . 3  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph ) )
2 sbie.1 . . . 4  |-  F/ x ps
3 sbie.2 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
43biimpa 471 . . . 4  |-  ( ( x  =  y  /\  ph )  ->  ps )
52, 4exlimi 1821 . . 3  |-  ( E. x ( x  =  y  /\  ph )  ->  ps )
61, 5syl 16 . 2  |-  ( [ y  /  x ] ph  ->  ps )
73biimprcd 217 . . . 4  |-  ( ps 
->  ( x  =  y  ->  ph ) )
82, 7alrimi 1781 . . 3  |-  ( ps 
->  A. x ( x  =  y  ->  ph )
)
9 sb2 2086 . . 3  |-  ( A. x ( x  =  y  ->  ph )  ->  [ y  /  x ] ph )
108, 9syl 16 . 2  |-  ( ps 
->  [ y  /  x ] ph )
116, 10impbii 181 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550   F/wnf 1553   [wsb 1658
This theorem is referenced by:  sbied  2125  equsb3lem  2177  elsb3  2179  elsb4  2180  cbveu  2301  mo4f  2313  2mos  2360  bm1.1  2421  eqsb3lem  2536  clelsb3  2538  cbvab  2554  cbvralf  2919  cbvreu  2923  sbralie  2938  cbvrab  2947  reu2  3115  nfcdeq  3151  sbcco2  3177  sbcie2g  3187  sbcralt  3226  sbcralg  3228  sbcrexg  3229  sbcreug  3230  sbcel12g  3259  sbceqg  3260  cbvralcsf  3304  cbvreucsf  3306  cbvrabcsf  3307  sbss  3730  sbcbrg  4254  cbvopab1  4271  cbvmpt  4292  tfis2f  4828  tfinds  4832  cbviota  5416  cbvriota  6553  nd1  8455  nd2  8456  clelsb3f  23964  rmo4fOLD  23976  rmo4f  23977  funcnv4mpt  24078  ballotlemodife  24748  setinds2f  25399  wfis2fg  25479  frins2fg  25515  prtlem5  26697  bnj1321  29334
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-sb 1659
  Copyright terms: Public domain W3C validator