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

Theorem sbie 1721
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 1457 . 2  |-  ( ps 
->  A. x ps )
3 sbie.2 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
42, 3sbieh 1720 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   F/wnf 1394   [wsb 1692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-i9 1468  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693
This theorem is referenced by:  cbveu  1972  mo4f  2008  bm1.1  2073  eqsb3lem  2190  clelsb3  2192  clelsb4  2193  cbvab  2210  clelsb3f  2232  cbvralf  2584  cbvrexf  2585  cbvreu  2588  sbralie  2603  cbvrab  2617  reu2  2801  rmo4f  2811  nfcdeq  2835  sbcco2  2860  sbcie2g  2870  sbcralt  2913  sbcrext  2914  sbcralg  2915  sbcreug  2917  sbcel12g  2944  sbceqg  2945  cbvralcsf  2988  cbvrexcsf  2989  cbvreucsf  2990  cbvrabcsf  2991  sbss  3386  disjiun  3832  sbcbrg  3886  cbvopab1  3903  cbvmpt  3925  tfis2f  4389  cbviota  4972  relelfvdm  5320  nfvres  5321  cbvriota  5600  bezoutlemnewy  11078  bezoutlemmain  11080
  Copyright terms: Public domain W3C validator