Theorem sbequ1 1939

Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sbequ1	|- ( x = y -> ( ph -> [ y / x ] ph ) )

Proof of Theorem sbequ1

Step	Hyp	Ref	Expression
1		pm3.4 545	. . 3 |- ( ( x = y /\ ph ) -> ( x = y -> ph ) )
2		19.8a 1758	. . 3 |- ( ( x = y /\ ph ) -> E. x ( x = y /\ ph ) )
3		df-sb 1656	. . 3 |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) )
4	1, 2, 3	sylanbrc 646	. 2 |- ( ( x = y /\ ph ) -> [ y / x ] ph )
5	4	ex 424	1 |- ( x = y -> ( ph -> [ y / x ] ph ) )

Syntax hints:   -> wi 4   /\ wa 359   E.wex 1547   [wsb 1655

This theorem is referenced by:  sbequ12  1940  dfsb2  2104  sbequi  2108  sbn  2111  sbi1  2112  sb6rf  2140  mo  2276  sb5ALT  28320  2pm13.193  28350  2pm13.193VD  28724  sb5ALTVD  28734  sbnNEW7  29266  sbi1NEW7  29267  sbequiNEW7  29282  sb6rfNEW7  29293  dfsb2NEW7  29339

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656