Theorem sbie 1815

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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1484  [wsb 1786

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-i9 1554  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787

This theorem is referenced by:  sbiev  1816  cbveu  2079  mo4f  2115  bm1.1  2191  eqsb1lem  2309  clelsb1  2311  clelsb2  2312  cbvab  2330  clelsb1f  2353  cbvralf  2731  cbvrexf  2732  cbvreu  2737  sbralie  2757  cbvrab  2771  reu2  2965  rmo4f  2975  nfcdeq  2999  sbcco2  3025  sbcie2g  3036  sbcralt  3079  sbcrext  3080  sbcralg  3081  sbcreug  3083  sbcel12g  3112  sbceqg  3113  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  sbss  3572  disjiun  4046  sbcbrg  4106  cbvopab1  4125  cbvmpt  4147  tfis2f  4640  cbviota  5246  relelfvdm  5621  nfvres  5623  cbvriota  5923  bezoutlemnewy  12392  bezoutlemmain  12394