Theorem sb2 1179

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 975	. . 3 |- (A.x(x = y -> ph) -> (x = y -> ph))
2		equs4 1152	. . 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 1174	. 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 956   = wceq 958  E.wex 982  [wsbc 1172

This theorem is referenced by:  stdpc4 1187  sb6x 1190  sbt 1194  equsb1 1195  equsb2 1196  sbied 1197  sb6f 1203  hbsb2a 1206  hbsb2e 1207  sb3 1224  sb4b 1226  dfsb2 1227  hbsb2 1229  sbn 1233  sbi1 1234  hbsb4 1250  sb6rf 1262  sbal1 1348

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174

Copyright terms: Public domain