Theorem sbie 1565

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 73	. 2 |- (ph -> ph)
2	1	hbth 1348	. . 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 1563	. 2 |- ((ph -> ph) -> ([y / x]ph <-> ps))
8	1, 7	ax-mp 7	1 |- ([y / x]ph <-> ps)

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298  [wsbc 1534

This theorem is referenced by:  dvelimf 1623  equsb3lem 1715  elsb3 1718  elsb4 1720  sb8euOLD 1784  cbveu 1785  mo4f 1798  2mos 1852  bm1.1 1870  eqsb3lem 1987  clelsb3 1990  cbvralf 2276  cbvrexf 2277  cbvreuv 2282  cbvab 2419  cbvrab 2421  reu2 2442  sbralie 2453  sbcco2 2468  sbcco2OLD 2469  sbcel1gvOLD 2511  sbcel2gv 2512  sbcel2gvOLD 2513  sbcralg 2531  sbcrexg 2533  sbcel12g 2552  sbceqdig 2554  sbss 2980  brab1 3384  sbcbrg 3390  cbvopab1 3405  posn 3603  tfis2f 3939  tfinds 3942  tfindsOLD 3943  tfinds2 3947  cbvmpt 5011  kmlem15 5941  nd1 6090  nd2 6091  bnj62 12433  bnj79 12440  bnj974 12859  bnj1377 13095  bnj1483 13160  bnj154 13245  bnj155 13246  bnj1123 13422  bnj1313 13494  bnj1319 13495  bnj1321 13498  bnj1373 13506  bnj1417 13530  setinds2f 13845  wfis2fg 13919  frins2fg 13943  soseq 13955  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  cbviotaf 16432

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