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

Theorem sbie 1749
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 𝑥𝜓
sbie.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
sbie ([𝑦 / 𝑥]𝜑𝜓)

Proof of Theorem sbie
StepHypRef Expression
1 sbie.1 . . 3 𝑥𝜓
21nfri 1484 . 2 (𝜓 → ∀𝑥𝜓)
3 sbie.2 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
42, 3sbieh 1748 1 ([𝑦 / 𝑥]𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wnf 1421  [wsb 1720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-i9 1495  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721
This theorem is referenced by:  cbveu  2001  mo4f  2037  bm1.1  2102  eqsb3lem  2220  clelsb3  2222  clelsb4  2223  cbvab  2240  clelsb3f  2262  cbvralf  2625  cbvrexf  2626  cbvreu  2629  sbralie  2644  cbvrab  2658  reu2  2845  rmo4f  2855  nfcdeq  2879  sbcco2  2904  sbcie2g  2914  sbcralt  2957  sbcrext  2958  sbcralg  2959  sbcreug  2961  sbcel12g  2988  sbceqg  2989  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  sbss  3441  disjiun  3894  sbcbrg  3952  cbvopab1  3971  cbvmpt  3993  tfis2f  4468  cbviota  5063  relelfvdm  5421  nfvres  5422  cbvriota  5708  bezoutlemnewy  11611  bezoutlemmain  11613
  Copyright terms: Public domain W3C validator