Theorem sbie 1791

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1460  [wsb 1762

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763

This theorem is referenced by:  sbiev  1792  cbveu  2050  mo4f  2086  bm1.1  2162  eqsb1lem  2280  clelsb1  2282  clelsb2  2283  cbvab  2301  clelsb1f  2323  cbvralf  2696  cbvrexf  2697  cbvreu  2701  sbralie  2721  cbvrab  2735  reu2  2925  rmo4f  2935  nfcdeq  2959  sbcco2  2985  sbcie2g  2996  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcreug  3043  sbcel12g  3072  sbceqg  3073  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  sbss  3531  disjiun  3996  sbcbrg  4055  cbvopab1  4074  cbvmpt  4096  tfis2f  4581  cbviota  5180  relelfvdm  5544  nfvres  5545  cbvriota  5836  bezoutlemnewy  11987  bezoutlemmain  11989