Theorem sbie 1765

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

Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1437  [wsb 1736

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-i9 1511  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737

This theorem is referenced by:  sbiev  1766  cbveu  2024  mo4f  2060  bm1.1  2125  eqsb3lem  2243  clelsb3  2245  clelsb4  2246  cbvab  2264  clelsb3f  2286  cbvralf  2651  cbvrexf  2652  cbvreu  2655  sbralie  2673  cbvrab  2687  reu2  2876  rmo4f  2886  nfcdeq  2910  sbcco2  2935  sbcie2g  2946  sbcralt  2989  sbcrext  2990  sbcralg  2991  sbcreug  2993  sbcel12g  3022  sbceqg  3023  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  sbss  3476  disjiun  3932  sbcbrg  3990  cbvopab1  4009  cbvmpt  4031  tfis2f  4506  cbviota  5101  relelfvdm  5461  nfvres  5462  cbvriota  5748  bezoutlemnewy  11720  bezoutlemmain  11722