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

Syntax hints:   → wi 4   ↔ wb 105  Ⅎwnf 1509  [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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-i9 1579  ax-ial 1583

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

This theorem is referenced by:  sbiev  1840  cbveu  2103  mo4f  2140  bm1.1  2216  eqsb1lem  2334  clelsb1  2336  clelsb2  2337  cbvab  2356  clelsb1f  2379  cbvralf  2759  cbvrexf  2760  cbvreu  2766  sbralie  2786  cbvrab  2801  reu2  2995  rmo4f  3005  nfcdeq  3029  sbcco2  3055  sbcie2g  3066  sbcralt  3109  sbcrext  3110  sbcralg  3111  sbcreug  3113  sbcel12g  3143  sbceqg  3144  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  sbss  3604  disjiun  4088  sbcbrg  4148  cbvopab1  4167  cbvmpt  4189  tfis2f  4688  cbviota  5298  relelfvdm  5680  nfvres  5684  cbvriota  5993  bezoutlemnewy  12630  bezoutlemmain  12632