Theorem sbie 2038

Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.)

Hypotheses

Ref	Expression
sbie.1	⊢ Ⅎxψ
sbie.2	⊢ (x = y → (φ ↔ ψ))

Assertion

Ref	Expression
sbie	⊢ ([y / x]φ ↔ ψ)

Proof of Theorem sbie

Step	Hyp	Ref	Expression
1		nftru 1554	. . 3 ⊢ Ⅎx ⊤
2		sbie.1	. . . 4 ⊢ Ⅎxψ
3	2	a1i 10	. . 3 ⊢ ( ⊤ → Ⅎxψ)
4		sbie.2	. . . 4 ⊢ (x = y → (φ ↔ ψ))
5	4	a1i 10	. . 3 ⊢ ( ⊤ → (x = y → (φ ↔ ψ)))
6	1, 3, 5	sbied 2036	. 2 ⊢ ( ⊤ → ([y / x]φ ↔ ψ))
7	6	trud 1323	1 ⊢ ([y / x]φ ↔ ψ)

Syntax hints:   → wi 4   ↔ wb 176   ⊤ wtru 1316  Ⅎwnf 1544  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by:  equsb3lem  2101  elsb3  2103  elsb4  2104  cbveu  2224  mo4f  2236  2mos  2283  bm1.1  2338  eqsb3lem  2453  clelsb3  2455  cbvab  2471  cbvralf  2829  cbvreu  2833  sbralie  2848  cbvrab  2857  reu2  3024  sbcco2  3069  sbcie2g  3079  sbcel2gv  3106  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  sbcel12g  3151  sbceqg  3152  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  sbss  3659  cbviota  4344  cbvopab1  4632  sbcbrg  4685  cbvmpt  5676  fvfullfunlem1  5861