Theorem sbied 1195

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

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	. . 3 |- (ph -> A.xph)
2		sbied.3	. . . . . . . . 9 |- (ph -> (x = y -> (ps <-> ch)))
3		bi1 148	. . . . . . . . 9 |- ((ps <-> ch) -> (ps -> ch))
4	2, 3	syl6 22	. . . . . . . 8 |- (ph -> (x = y -> (ps -> ch)))
5	4	imp3a 361	. . . . . . 7 |- (ph -> ((x = y /\ ps) -> ch))
6	5	19.20i 992	. . . . . 6 |- (A.xph -> A.x((x = y /\ ps) -> ch))
7		19.22 1039	. . . . . 6 |- (A.x((x = y /\ ps) -> ch) -> (E.x(x = y /\ ps) -> E.xch))
8	6, 7	syl 10	. . . . 5 |- (A.xph -> (E.x(x = y /\ ps) -> E.xch))
9		sb1 1176	. . . . 5 |- ([y / x]ps -> E.x(x = y /\ ps))
10	8, 9	syl5 21	. . . 4 |- (A.xph -> ([y / x]ps -> E.xch))
11		sbied.2	. . . . . . 7 |- (ph -> (ch -> A.xch))
12	11	19.20i 992	. . . . . 6 |- (A.xph -> A.x(ch -> A.xch))
13		hba1 1003	. . . . . . 7 |- (A.xch -> A.xA.xch)
14	13	19.23 1063	. . . . . 6 |- (A.x(ch -> A.xch) <-> (E.xch -> A.xch))
15	12, 14	sylib 198	. . . . 5 |- (A.xph -> (E.xch -> A.xch))
16		ax-4 973	. . . . 5 |- (A.xch -> ch)
17	15, 16	syl6 22	. . . 4 |- (A.xph -> (E.xch -> ch))
18	10, 17	syld 27	. . 3 |- (A.xph -> ([y / x]ps -> ch))
19	1, 18	syl 10	. 2 |- (ph -> ([y / x]ps -> ch))
20	11	a4s 984	. . . 4 |- (A.xph -> (ch -> A.xch))
21		bi2 149	. . . . . . . 8 |- ((ps <-> ch) -> (ch -> ps))
22	2, 21	syl6 22	. . . . . . 7 |- (ph -> (x = y -> (ch -> ps)))
23	22	com23 32	. . . . . 6 |- (ph -> (ch -> (x = y -> ps)))
24	23	19.20ii 995	. . . . 5 |- (A.xph -> (A.xch -> A.x(x = y -> ps)))
25		sb2 1177	. . . . 5 |- (A.x(x = y -> ps) -> [y / x]ps)
26	24, 25	syl6 22	. . . 4 |- (A.xph -> (A.xch -> [y / x]ps))
27	20, 26	syld 27	. . 3 |- (A.xph -> (ch -> [y / x]ps))
28	1, 27	syl 10	. 2 |- (ph -> (ch -> [y / x]ps))
29	19, 28	impbid 516	1 |- (ph -> ([y / x]ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 954   = wceq 956  E.wex 980  [wsbc 1170

This theorem is referenced by:  sbie 1196  dvelimdf 1251  sbidm 1254  sbco2 1255

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172

Copyright terms: Public domain