Metamath Proof Explorer


Theorem sbc6g

Description: An equivalence for class substitution. (Contributed by NM, 11-Oct-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Assertion sbc6g A V [˙A / x]˙ φ x x = A φ

Proof

Step Hyp Ref Expression
1 alexeqg A V x x = A φ x x = A φ
2 sbc5 [˙A / x]˙ φ x x = A φ
3 1 2 syl6rbbr A V [˙A / x]˙ φ x x = A φ