Theorem sb2 1175

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		ax-4 971	. . 3 |- (A.x(x = y -> ph) -> (x = y -> ph))
2		equs4 1148	. . 3 |- (A.x(x = y -> ph) -> E.x(x = y /\ ph))
3	1, 2	jca 288	. 2 |- (A.x(x = y -> ph) -> ((x = y -> ph) /\ E.x(x = y /\ ph)))
4		df-sb 1170	. 2 |- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
5	3, 4	sylibr 200	1 |- (A.x(x = y -> ph) -> [y / x]ph)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 952   = wceq 954  E.wex 978  [wsbc 1168

This theorem is referenced by:  stdpc4 1183  sb6x 1186  sbt 1190  equsb1 1191  equsb2 1192  sbied 1193  sb6f 1199  hbsb2a 1202  hbsb2e 1203  sb3 1220  sb4b 1222  dfsb2 1223  hbsb2 1225  sbn 1229  sbi1 1230  hbsb4 1246  sb6rf 1258  sbal1 1344

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain