ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbie Unicode version

Theorem sbie 1789
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 sbie.1 . . 3  |-  F/ x ps
21nfri 1517 . 2  |-  ( ps 
->  A. x ps )
3 sbie.2 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
42, 3sbieh 1788 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   F/wnf 1458   [wsb 1760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-i9 1528  ax-ial 1532
This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761
This theorem is referenced by:  sbiev  1790  cbveu  2048  mo4f  2084  bm1.1  2160  eqsb1lem  2278  clelsb1  2280  clelsb2  2281  cbvab  2299  clelsb1f  2321  cbvralf  2694  cbvrexf  2695  cbvreu  2699  sbralie  2719  cbvrab  2733  reu2  2923  rmo4f  2933  nfcdeq  2957  sbcco2  2983  sbcie2g  2994  sbcralt  3037  sbcrext  3038  sbcralg  3039  sbcreug  3041  sbcel12g  3070  sbceqg  3071  cbvralcsf  3117  cbvrexcsf  3118  cbvreucsf  3119  cbvrabcsf  3120  sbss  3529  disjiun  3993  sbcbrg  4052  cbvopab1  4071  cbvmpt  4093  tfis2f  4577  cbviota  5175  relelfvdm  5539  nfvres  5540  cbvriota  5831  bezoutlemnewy  11963  bezoutlemmain  11965
  Copyright terms: Public domain W3C validator