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

Theorem sbie 1745
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 1480 . 2  |-  ( ps 
->  A. x ps )
3 sbie.2 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
42, 3sbieh 1744 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   F/wnf 1417   [wsb 1716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-i9 1491  ax-ial 1495
This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717
This theorem is referenced by:  cbveu  1997  mo4f  2033  bm1.1  2098  eqsb3lem  2215  clelsb3  2217  clelsb4  2218  cbvab  2235  clelsb3f  2257  cbvralf  2620  cbvrexf  2621  cbvreu  2624  sbralie  2639  cbvrab  2653  reu2  2839  rmo4f  2849  nfcdeq  2873  sbcco2  2898  sbcie2g  2908  sbcralt  2951  sbcrext  2952  sbcralg  2953  sbcreug  2955  sbcel12g  2982  sbceqg  2983  cbvralcsf  3026  cbvrexcsf  3027  cbvreucsf  3028  cbvrabcsf  3029  sbss  3435  disjiun  3888  sbcbrg  3942  cbvopab1  3959  cbvmpt  3981  tfis2f  4456  cbviota  5049  relelfvdm  5405  nfvres  5406  cbvriota  5692  bezoutlemnewy  11524  bezoutlemmain  11526
  Copyright terms: Public domain W3C validator