Theorem stdpc4 2353

Description: The specialization axiom of standard predicate calculus. It states that if a statement ph holds for all x, then it also holds for the specific case of y (properly) substituted for x. Translated to traditional notation, it can be read: " A. x ph ( x ) -> ph ( y ), provided that y is free for x in ph ( x )." Axiom 4 of [Mendelson] p. 69. See also spsbc 3448 and rspsbc 3518. (Contributed by NM, 14-May-1993.)

Assertion

Ref	Expression
stdpc4	|- ( A. x ph -> [ y / x ] ph )

Proof of Theorem stdpc4

Step	Hyp	Ref	Expression
1		ala1 1741	. 2 |- ( A. x ph -> A. x ( x = y -> ph ) )
2		sb2 2352	. 2 |- ( A. x ( x = y -> ph ) -> [ y / x ] ph )
3	1, 2	syl 17	1 |- ( A. x ph -> [ y / x ] ph )

Syntax hints:   -> wi 4   A.wal 1481   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-sb 1881

This theorem is referenced by:  2stdpc4  2354  sbft  2379  spsbim  2394  spsbbi  2402  sbt  2419  sbtrt  2420  pm13.183  3344  spsbc  3448  nd1  9409  nd2  9410  bj-vexwt  32854  axfrege58b  38194  pm10.14  38558  pm11.57  38589