Theorem sbie 904

Description: Conversion of implicit substitution to explicit substitution.

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		id 9	. 2 ⊢ (φ → φ)
2	1	hbth 697	. . 3 ⊢ ((φ → φ) → ∀x(φ → φ))
3		sbie.1	. . . 4 ⊢ (ψ → ∀xψ)
4	3	a1i 7	. . 3 ⊢ ((φ → φ) → (ψ → ∀xψ))
5		sbie.2	. . . 4 ⊢ (x = y → (φ ↔ ψ))
6	5	a1i 7	. . 3 ⊢ ((φ → φ) → (x = y → (φ ↔ ψ)))
7	2, 4, 6	sbied 903	. 2 ⊢ ((φ → φ) → ([y / x]φ ↔ ψ))
8	1, 7	ax-mp 6	1 ⊢ ([y / x]φ ↔ ψ)

Syntax hints:   → wi 2   ↔ wb 127  ∀wal 672   = weq 797  [wsb 852

This theorem is referenced by:  ddelimf 908  sb8eu 1017  cbveu 1018  mo4f 1028  bm1.1 1088  reu2 1338  reu4 1340  sbralie 1439  sbcco2 1449  tfis2f 2246  tfinds 2401  tfinds2 2405  kmlem15 3594  nd1 3732  nd2 3733

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org