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

Theorem sbie 1978
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 1541 . . 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 1976 . 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 1531   [wsb 1629
This theorem is referenced by:  equsb3lem  2040  elsb3  2042  elsb4  2043  cbveu  2163  mo4f  2175  2mos  2222  bm1.1  2268  eqsb3lem  2383  clelsb3  2385  cbvab  2401  cbvralf  2758  cbvreu  2762  sbralie  2777  cbvrab  2786  reu2  2953  nfcdeq  2988  sbcco2  3014  sbcie2g  3024  sbcel2gv  3051  sbcralt  3063  sbcralg  3065  sbcrexg  3066  sbcreug  3067  sbcel12g  3096  sbceqg  3097  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  sbss  3563  sbcbrg  4072  cbvopab1  4089  cbvmpt  4110  tfis2f  4646  tfisi  4649  tfinds  4650  cbviota  5224  cbvriota  6315  nd1  8209  nd2  8210  ballotlemodife  23056  clelsb3f  23142  rmo4fOLD  23179  rmo4f  23180  cbvmptf  23220  funcnv4mpt  23237  setinds2f  24135  wfis2fg  24211  frins2fg  24247  prtlem5  26722  bnj1321  29057
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630
  Copyright terms: Public domain W3C validator