Metamath Proof Explorer


Theorem sbceq1a

Description: Equality theorem for class substitution. Class version of sbequ12 . (Contributed by NM, 26-Sep-2003)

Ref Expression
Assertion sbceq1a x=Aφ[˙A/x]˙φ

Proof

Step Hyp Ref Expression
1 sbid xxφφ
2 dfsbcq2 x=Axxφ[˙A/x]˙φ
3 1 2 bitr3id x=Aφ[˙A/x]˙φ