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

Theorem sbie 1715
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 1453 . 2  |-  ( ps 
->  A. x ps )
3 sbie.2 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
42, 3sbieh 1714 1  |-  ( [ y  /  x ] ph 
<->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   F/wnf 1390   [wsb 1686
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-i9 1464  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687
This theorem is referenced by:  cbveu  1966  mo4f  2002  bm1.1  2067  eqsb3lem  2182  clelsb3  2184  clelsb4  2185  cbvab  2202  cbvralf  2572  cbvrexf  2573  cbvreu  2576  sbralie  2591  cbvrab  2600  reu2  2781  nfcdeq  2813  sbcco2  2838  sbcie2g  2848  sbcralt  2891  sbcrext  2892  sbcralg  2893  sbcreug  2895  sbcel12g  2922  sbceqg  2923  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  sbss  3357  sbcbrg  3842  cbvopab1  3859  cbvmpt  3880  tfis2f  4333  cbviota  4902  relelfvdm  5237  nfvres  5238  cbvriota  5509  bezoutlemnewy  10529  bezoutlemmain  10531
  Copyright terms: Public domain W3C validator