Theorem sbied 2036

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

Hypotheses

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

Assertion

Ref	Expression
sbied	⊢ (φ → ([y / x]ψ ↔ χ))

Proof of Theorem sbied

Step	Hyp	Ref	Expression
1		sb1 1651	. . . 4 ⊢ ([y / x]ψ → ∃x(x = y ∧ ψ))
2		sbied.1	. . . . 5 ⊢ Ⅎxφ
3		sbied.3	. . . . . . 7 ⊢ (φ → (x = y → (ψ ↔ χ)))
4		bi1 178	. . . . . . 7 ⊢ ((ψ ↔ χ) → (ψ → χ))
5	3, 4	syl6 29	. . . . . 6 ⊢ (φ → (x = y → (ψ → χ)))
6	5	imp3a 420	. . . . 5 ⊢ (φ → ((x = y ∧ ψ) → χ))
7	2, 6	eximd 1770	. . . 4 ⊢ (φ → (∃x(x = y ∧ ψ) → ∃xχ))
8	1, 7	syl5 28	. . 3 ⊢ (φ → ([y / x]ψ → ∃xχ))
9		sbied.2	. . . 4 ⊢ (φ → Ⅎxχ)
10	9	19.9d 1782	. . 3 ⊢ (φ → (∃xχ → χ))
11	8, 10	syld 40	. 2 ⊢ (φ → ([y / x]ψ → χ))
12	9	nfrd 1763	. . 3 ⊢ (φ → (χ → ∀xχ))
13		bi2 189	. . . . . . 7 ⊢ ((ψ ↔ χ) → (χ → ψ))
14	3, 13	syl6 29	. . . . . 6 ⊢ (φ → (x = y → (χ → ψ)))
15	14	com23 72	. . . . 5 ⊢ (φ → (χ → (x = y → ψ)))
16	2, 15	alimd 1764	. . . 4 ⊢ (φ → (∀xχ → ∀x(x = y → ψ)))
17		sb2 2023	. . . 4 ⊢ (∀x(x = y → ψ) → [y / x]ψ)
18	16, 17	syl6 29	. . 3 ⊢ (φ → (∀xχ → [y / x]ψ))
19	12, 18	syld 40	. 2 ⊢ (φ → (χ → [y / x]ψ))
20	11, 19	impbid 183	1 ⊢ (φ → ([y / x]ψ ↔ χ))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541  Ⅎwnf 1544  [wsb 1648

This proof depends on 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 proof depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is used by:  sbiedv  2037  sbie  2038  dvelimdf  2082  sbco2  2086