Theorem sbie 1192

Description: Conversion of implicit substitution to explicit substitution.

Hypotheses

Ref	Expression
sbie.1	|- (ps -> A.xps)
sbie.2	|- (x = y -> (ph <-> ps))

Assertion

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

Proof of Theorem sbie

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2	1	hbth 998	. . 3 |- ((ph -> ph) -> A.x(ph -> ph))
3		sbie.1	. . . 4 |- (ps -> A.xps)
4	3	a1i 8	. . 3 |- ((ph -> ph) -> (ps -> A.xps))
5		sbie.2	. . . 4 |- (x = y -> (ph <-> ps))
6	5	a1i 8	. . 3 |- ((ph -> ph) -> (x = y -> (ph <-> ps)))
7	2, 4, 6	sbied 1191	. 2 |- ((ph -> ph) -> ([y / x]ph <-> ps))
8	1, 7	ax-mp 7	1 |- ([y / x]ph <-> ps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951   = wceq 953  [wsbc 1166

This theorem is referenced by:  dvelimf 1245  sb8eu 1383  cbveu 1384  mo4f 1395  2mos 1441  bm1.1 1455  reu2 1920  sbralie 1931  sbcco2 1943  sbcel1gv 1970  sbcel2gv 1971  tfis2f 3118  tfinds 3151  tfinds2 3155  kmlem15 4751  nd1 4910  nd2 4911

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168

Copyright terms: Public domain