Theorem sbied 1193

Description: Conversion of implicit substitution to explicit substitution (deduction version of sbie 1194).

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		sbied.1	. . 3 ⊢ (φ → ∀xφ)
2		sbied.3	. . . . . . . . 9 ⊢ (φ → (x = y → (ψ ↔ χ)))
3		bi1 148	. . . . . . . . 9 ⊢ ((ψ ↔ χ) → (ψ → χ))
4	2, 3	syl6 22	. . . . . . . 8 ⊢ (φ → (x = y → (ψ → χ)))
5	4	imp3a 361	. . . . . . 7 ⊢ (φ → ((x = y ⋀ ψ) → χ))
6	5	19.20i 990	. . . . . 6 ⊢ (∀xφ → ∀x((x = y ⋀ ψ) → χ))
7		19.22 1037	. . . . . 6 ⊢ (∀x((x = y ⋀ ψ) → χ) → (∃x(x = y ⋀ ψ) → ∃xχ))
8	6, 7	syl 10	. . . . 5 ⊢ (∀xφ → (∃x(x = y ⋀ ψ) → ∃xχ))
9		sb1 1174	. . . . 5 ⊢ ([y / x]ψ → ∃x(x = y ⋀ ψ))
10	8, 9	syl5 21	. . . 4 ⊢ (∀xφ → ([y / x]ψ → ∃xχ))
11		sbied.2	. . . . . . 7 ⊢ (φ → (χ → ∀xχ))
12	11	19.20i 990	. . . . . 6 ⊢ (∀xφ → ∀x(χ → ∀xχ))
13		hba1 1001	. . . . . . 7 ⊢ (∀xχ → ∀x∀xχ)
14	13	19.23 1061	. . . . . 6 ⊢ (∀x(χ → ∀xχ) ↔ (∃xχ → ∀xχ))
15	12, 14	sylib 198	. . . . 5 ⊢ (∀xφ → (∃xχ → ∀xχ))
16		ax-4 971	. . . . 5 ⊢ (∀xχ → χ)
17	15, 16	syl6 22	. . . 4 ⊢ (∀xφ → (∃xχ → χ))
18	10, 17	syld 27	. . 3 ⊢ (∀xφ → ([y / x]ψ → χ))
19	1, 18	syl 10	. 2 ⊢ (φ → ([y / x]ψ → χ))
20	11	a4s 982	. . . 4 ⊢ (∀xφ → (χ → ∀xχ))
21		bi2 149	. . . . . . . 8 ⊢ ((ψ ↔ χ) → (χ → ψ))
22	2, 21	syl6 22	. . . . . . 7 ⊢ (φ → (x = y → (χ → ψ)))
23	22	com23 32	. . . . . 6 ⊢ (φ → (χ → (x = y → ψ)))
24	23	19.20ii 993	. . . . 5 ⊢ (∀xφ → (∀xχ → ∀x(x = y → ψ)))
25		sb2 1175	. . . . 5 ⊢ (∀x(x = y → ψ) → [y / x]ψ)
26	24, 25	syl6 22	. . . 4 ⊢ (∀xφ → (∀xχ → [y / x]ψ))
27	20, 26	syld 27	. . 3 ⊢ (∀xφ → (χ → [y / x]ψ))
28	1, 27	syl 10	. 2 ⊢ (φ → (χ → [y / x]ψ))
29	19, 28	impbid 515	1 ⊢ (φ → ([y / x]ψ ↔ χ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954  ∃wex 978  [wsbc 1168

This theorem is referenced by:  sbie 1194  dvelimdf 1249  sbidm 1252  sbco2 1253

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain