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	|- F/xph
sbied.2	|- (ph -> F/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		sb1 1651	. . . 4 |- ([y / x]ps -> E.x(x = y /\ ps))
2		sbied.1	. . . . 5 |- F/xph
3		sbied.3	. . . . . . 7 |- (ph -> (x = y -> (ps <-> ch)))
4		bi1 178	. . . . . . 7 |- ((ps <-> ch) -> (ps -> ch))
5	3, 4	syl6 29	. . . . . 6 |- (ph -> (x = y -> (ps -> ch)))
6	5	imp3a 420	. . . . 5 |- (ph -> ((x = y /\ ps) -> ch))
7	2, 6	eximd 1770	. . . 4 |- (ph -> (E.x(x = y /\ ps) -> E.xch))
8	1, 7	syl5 28	. . 3 |- (ph -> ([y / x]ps -> E.xch))
9		sbied.2	. . . 4 |- (ph -> F/xch)
10	9	19.9d 1782	. . 3 |- (ph -> (E.xch -> ch))
11	8, 10	syld 40	. 2 |- (ph -> ([y / x]ps -> ch))
12	9	nfrd 1763	. . 3 |- (ph -> (ch -> A.xch))
13		bi2 189	. . . . . . 7 |- ((ps <-> ch) -> (ch -> ps))
14	3, 13	syl6 29	. . . . . 6 |- (ph -> (x = y -> (ch -> ps)))
15	14	com23 72	. . . . 5 |- (ph -> (ch -> (x = y -> ps)))
16	2, 15	alimd 1764	. . . 4 |- (ph -> (A.xch -> A.x(x = y -> ps)))
17		sb2 2023	. . . 4 |- (A.x(x = y -> ps) -> [y / x]ps)
18	16, 17	syl6 29	. . 3 |- (ph -> (A.xch -> [y / x]ps))
19	12, 18	syld 40	. 2 |- (ph -> (ch -> [y / x]ps))
20	11, 19	impbid 183	1 |- (ph -> ([y / x]ps <-> ch))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   F/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:  sbiedv  2037  sbie  2038  dvelimdf  2082  sbco2  2086