Theorem sbied 1563

Description: Conversion of implicit substitution to explicit substitution (deduction version of sbie 1565). (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
sbied.1	|- (ph -> A.xph)
sbied.2	|- (ph -> (ch -> A.xch))
sbied.3	|- (ph -> (x = y -> (ps <-> ch)))

Assertion

Ref	Expression
sbied	|- (ph -> ([y / x]ps <-> ch))

Proof of Theorem sbied

Step	Hyp	Ref	Expression
1		sbied.1	. . . . 5 |- (ph -> A.xph)
2		sbied.3	. . . . . . 7 |- (ph -> (x = y -> (ps <-> ch)))
3		bi1 165	. . . . . . 7 |- ((ps <-> ch) -> (ps -> ch))
4	2, 3	syl6 25	. . . . . 6 |- (ph -> (x = y -> (ps -> ch)))
5	4	imp3a 388	. . . . 5 |- (ph -> ((x = y /\ ps) -> ch))
6	1, 5	eximd 1410	. . . 4 |- (ph -> (E.x(x = y /\ ps) -> E.xch))
7		sb1 1540	. . . 4 |- ([y / x]ps -> E.x(x = y /\ ps))
8	6, 7	syl5 20	. . 3 |- (ph -> ([y / x]ps -> E.xch))
9		sbied.2	. . . 4 |- (ph -> (ch -> A.xch))
10	1, 9	19.9d 1384	. . 3 |- (ph -> (E.xch -> ch))
11	8, 10	syld 30	. 2 |- (ph -> ([y / x]ps -> ch))
12		bi2 166	. . . . . . 7 |- ((ps <-> ch) -> (ch -> ps))
13	2, 12	syl6 25	. . . . . 6 |- (ph -> (x = y -> (ch -> ps)))
14	13	com23 36	. . . . 5 |- (ph -> (ch -> (x = y -> ps)))
15	1, 14	alimd 1343	. . . 4 |- (ph -> (A.xch -> A.x(x = y -> ps)))
16		sb2 1541	. . . 4 |- (A.x(x = y -> ps) -> [y / x]ps)
17	15, 16	syl6 25	. . 3 |- (ph -> (A.xch -> [y / x]ps))
18	9, 17	syld 30	. 2 |- (ph -> (ch -> [y / x]ps))
19	11, 18	impbid 574	1 |- (ph -> ([y / x]ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298  E.wex 1326  [wsbc 1534

This theorem is referenced by:  sbie 1565  dvelimdf 1624  sbidmOLD 1628  sbco2 1629

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536

Copyright terms: Public domain