Theorem sbie 1764

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

Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1436  [wsb 1735

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736

This theorem is referenced by:  sbiev  1765  cbveu  2021  mo4f  2057  bm1.1  2122  eqsb3lem  2240  clelsb3  2242  clelsb4  2243  cbvab  2261  clelsb3f  2283  cbvralf  2646  cbvrexf  2647  cbvreu  2650  sbralie  2665  cbvrab  2679  reu2  2867  rmo4f  2877  nfcdeq  2901  sbcco2  2926  sbcie2g  2937  sbcralt  2980  sbcrext  2981  sbcralg  2982  sbcreug  2984  sbcel12g  3012  sbceqg  3013  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  sbss  3466  disjiun  3919  sbcbrg  3977  cbvopab1  3996  cbvmpt  4018  tfis2f  4493  cbviota  5088  relelfvdm  5446  nfvres  5447  cbvriota  5733  bezoutlemnewy  11673  bezoutlemmain  11675