Theorem pm13.13a 38608

Description: One result of theorem *13.13 in [WhiteheadRussell] p. 178. A note on the section - to make the theorems more usable, and because inequality is notation for set theory (it is not defined in the predicate calculus section), this section will use classes instead of sets. (Contributed by Andrew Salmon, 3-Jun-2011.)

Assertion

Ref	Expression
pm13.13a	|- ( ( ph /\ x = A ) -> [. A / x ]. ph )

Proof of Theorem pm13.13a

Step	Hyp	Ref	Expression
1		sbceq1a 3446	. 2 |- ( x = A -> ( ph <-> [. A / x ]. ph ) )
2	1	biimpac 503	1 |- ( ( ph /\ x = A ) -> [. A / x ]. ph )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   [.wsbc 3435

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-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  pm13.194  38613