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	⊢ Ⅎ𝑥𝜓
sbie.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbie	⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)

Proof of Theorem sbie

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

Syntax hints:   → wi 4   ↔ wb 103  Ⅎ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