This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm13.13a

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)

Ref Expression
Assertion pm13.13a ⊢ φ ∧ x = A → [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 sbceq1a ⊢ x = A → φ ↔ [˙A / x]˙ φ
2 1 biimpac ⊢ φ ∧ x = A → [˙A / x]˙ φ