Theorem sb2 1214

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 1009	. . 3 |- (A.x(x = y -> ph) -> (x = y -> ph))
2		equs4 1187	. . 3 |- (A.x(x = y -> ph) -> E.x(x = y /\ ph))
3	1, 2	jca 286	. 2 |- (A.x(x = y -> ph) -> ((x = y -> ph) /\ E.x(x = y /\ ph)))
4		df-sb 1209	. 2 |- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
5	3, 4	sylibr 198	1 |- (A.x(x = y -> ph) -> [y / x]ph)

Syntax hints:   -> wi 3   /\ wa 221  A.wal 990   = wceq 992  E.wex 1016  [wsbc 1207

This theorem is referenced by:  stdpc4 1222  sb6x 1225  sbt 1229  equsb1 1230  equsb2 1231  sbied 1232  sb6f 1238  hbsb2a 1241  hbsb2e 1242  sb3 1259  sb4b 1261  dfsb2 1262  hbsb2 1264  sbn 1268  sbi1 1269  hbsb4 1286  sb6rf 1298  sbal1 1385

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209

Copyright terms: Public domain