Theorem sbie 1839

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1508  [wsb 1810

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-i9 1578  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811

This theorem is referenced by:  sbiev  1840  cbveu  2103  mo4f  2140  bm1.1  2216  eqsb1lem  2334  clelsb1  2336  clelsb2  2337  cbvab  2355  clelsb1f  2378  cbvralf  2758  cbvrexf  2759  cbvreu  2765  sbralie  2785  cbvrab  2800  reu2  2994  rmo4f  3004  nfcdeq  3028  sbcco2  3054  sbcie2g  3065  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcreug  3112  sbcel12g  3142  sbceqg  3143  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  sbss  3602  disjiun  4083  sbcbrg  4143  cbvopab1  4162  cbvmpt  4184  tfis2f  4682  cbviota  5291  relelfvdm  5671  nfvres  5675  cbvriota  5982  bezoutlemnewy  12566  bezoutlemmain  12568