Theorem sbie 1714

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 1452	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		sbie.2	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	2, 3	sbieh 1713	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 103  Ⅎwnf 1389  [wsb 1685

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-i9 1463  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686

This theorem is referenced by:  cbveu  1965  mo4f  2001  bm1.1  2066  eqsb3lem  2181  clelsb3  2183  clelsb4  2184  cbvab  2201  cbvralf  2571  cbvrexf  2572  cbvreu  2575  sbralie  2590  cbvrab  2599  reu2  2780  nfcdeq  2812  sbcco2  2837  sbcie2g  2847  sbcralt  2890  sbcrext  2891  sbcralg  2892  sbcreug  2894  sbcel12g  2921  sbceqg  2922  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  sbss  3349  sbcbrg  3834  cbvopab1  3851  cbvmpt  3872  tfis2f  4325  cbviota  4892  relelfvdm  5226  nfvres  5227  cbvriota  5498  bezoutlemnewy  10385  bezoutlemmain  10387