Theorem sb2 1541

Description: One direction of a simplified definition of substitution.

Assertion

Ref	Expression
sb2	|- (A.x(x = y -> ph) -> [y / x]ph)

Proof of Theorem sb2

Step	Hyp	Ref	Expression
1		df-sb 1536	. 2 |- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
2		ax-4 1319	. 2 |- (A.x(x = y -> ph) -> (x = y -> ph))
3		equs4 1510	. 2 |- (A.x(x = y -> ph) -> E.x(x = y /\ ph))
4	1, 2, 3	sylanbrc 527	1 |- (A.x(x = y -> ph) -> [y / x]ph)

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298  E.wex 1326  [wsbc 1534

This theorem is referenced by:  stdpc4 1550  sb6xOLD 1554  sbtOLD 1560  equsb1 1561  equsb2 1562  sbied 1563  sbiedOLD 1564  sb6f 1570  hbsb2a 1573  hbsb2e 1574  sb3 1592  sb4b 1594  dfsb2 1595  hbsb2 1597  sbn 1601  sbi1 1602  hbsb4 1620  sb6rf 1635  sb6rfOLD 1636  sbal1 1737  iota4 5100  sbeqal1 16355  euunianOLD 16396

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