Theorem sb2 1173

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 970	. . 3 |- (A.x(x = y -> ph) -> (x = y -> ph))
2		equs4 1146	. . 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 1168	. 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 951   = wceq 953  E.wex 977  [wsbc 1166

This theorem is referenced by:  stdpc4 1181  sb6x 1184  sbt 1188  equsb1 1189  equsb2 1190  sbied 1191  sb6f 1197  hbsb2a 1200  hbsb2e 1201  sb3 1217  sb4b 1219  dfsb2 1220  hbsb2 1222  sbn 1226  sbi1 1227  hbsb4 1243  sb6rf 1255  sbal1 1341

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