Theorem sbie 1813

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1482  [wsb 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-i9 1552  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785

This theorem is referenced by:  sbiev  1814  cbveu  2077  mo4f  2113  bm1.1  2189  eqsb1lem  2307  clelsb1  2309  clelsb2  2310  cbvab  2328  clelsb1f  2351  cbvralf  2729  cbvrexf  2730  cbvreu  2735  sbralie  2755  cbvrab  2769  reu2  2960  rmo4f  2970  nfcdeq  2994  sbcco2  3020  sbcie2g  3031  sbcralt  3074  sbcrext  3075  sbcralg  3076  sbcreug  3078  sbcel12g  3107  sbceqg  3108  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  sbss  3567  disjiun  4038  sbcbrg  4097  cbvopab1  4116  cbvmpt  4138  tfis2f  4630  cbviota  5234  relelfvdm  5602  nfvres  5604  cbvriota  5900  bezoutlemnewy  12236  bezoutlemmain  12238