Theorem sbf 1551

Description: Substitution for a variable not free in a wff does not affect it.

Hypothesis

Ref	Expression
sbf.1	|- (ph -> A.xph)

Assertion

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

Proof of Theorem sbf

Step	Hyp	Ref	Expression
1		sb1 1540	. . . 4 |- ([y / x]ph -> E.x(x = y /\ ph))
2		sbf.1	. . . . 5 |- (ph -> A.xph)
3	2	19.41 1448	. . . 4 |- (E.x(x = y /\ ph) <-> (E.x x = y /\ ph))
4	1, 3	sylib 215	. . 3 |- ([y / x]ph -> (E.x x = y /\ ph))
5	4	simprd 352	. 2 |- ([y / x]ph -> ph)
6		stdpc4 1550	. . 3 |- (A.xph -> [y / x]ph)
7	2, 6	syl 12	. 2 |- (ph -> [y / x]ph)
8	5, 7	impbii 174	1 |- ([y / x]ph <-> ph)

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

This theorem is referenced by:  sbf2 1552  sb6x 1553  sb6xOLD 1554  hbs1f 1555  sbequ5 1557  sbequ6 1558  sbt 1559  sb19.21 1606  sbrbif 1612  sbid2 1626  sb6rfOLD 1636  equsb3lemOLD 1716  elsb3 1718  elsb3OLD 1719  elsb4 1720  elsb4OLD 1721  sbmo 1796  eqsb3lemOLD 1988  clelsb3 1990  clelsb3OLD 1991  sbabel 2016  sbcgf 2520  sbcgfOLD 2521  sbsslem 2978  sbsslemOLD 2979  bnj34 12403  bnj37 12407  bnj37OLD 12408  bnj58 12431  bnj77 12437  bnj77OLD 12438  bnj1483 13160  bnj81 13209  bnj82 13210  bnj86 13213  bnj1037 13386  bnj1039 13387  sbmoOLD 15654  prtlem5 16245

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