Theorem sbie 1784

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

Step	Hyp	Ref	Expression
1		sbie.1	. . 3 ⊢ Ⅎ𝑥𝜓
2	1	nfri 1512	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		sbie.2	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	sbieh 1783	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1453  [wsb 1755

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-i9 1523  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756

This theorem is referenced by:  sbiev  1785  cbveu  2043  mo4f  2079  bm1.1  2155  eqsb1lem  2273  clelsb1  2275  clelsb2  2276  cbvab  2294  clelsb1f  2316  cbvralf  2689  cbvrexf  2690  cbvreu  2694  sbralie  2714  cbvrab  2728  reu2  2918  rmo4f  2928  nfcdeq  2952  sbcco2  2977  sbcie2g  2988  sbcralt  3031  sbcrext  3032  sbcralg  3033  sbcreug  3035  sbcel12g  3064  sbceqg  3065  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  sbss  3523  disjiun  3984  sbcbrg  4043  cbvopab1  4062  cbvmpt  4084  tfis2f  4568  cbviota  5165  relelfvdm  5528  nfvres  5529  cbvriota  5819  bezoutlemnewy  11951  bezoutlemmain  11953