Theorem sbie 1844

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1513  [wsb 1815

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-i9 1583  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816

This theorem is referenced by:  sbiev  1845  cbveu  2110  mo4f  2147  bm1.1  2223  eqsb1lem  2341  clelsb1  2343  clelsb2  2344  cbvab  2364  clelsb1f  2396  cbvralf  2777  cbvrexf  2778  cbvreu  2784  sbralie  2804  cbvrab  2819  reu2  3014  rmo4f  3024  nfcdeq  3048  sbcco2  3074  sbcie2g  3085  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcreug  3132  sbcel12g  3162  sbceqg  3163  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  sbss  3632  disjiun  4120  sbcbrg  4180  cbvopab1  4199  cbvmpt  4221  tfis2f  4726  cbviota  5337  relelfvdm  5722  nfvres  5726  cbvriota  6040  bezoutlemnewy  12751  bezoutlemmain  12753