Metamath Proof Explorer


Theorem sbceqi

Description: Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

Ref Expression
Hypotheses sbceqi.1 A V
sbceqi.2 A / x B = D
sbceqi.3 A / x C = E
Assertion sbceqi [˙A / x]˙ B = C D = E

Proof

Step Hyp Ref Expression
1 sbceqi.1 A V
2 sbceqi.2 A / x B = D
3 sbceqi.3 A / x C = E
4 sbceqg A V [˙A / x]˙ B = C A / x B = A / x C
5 1 4 ax-mp [˙A / x]˙ B = C A / x B = A / x C
6 2 3 eqeq12i A / x B = A / x C D = E
7 5 6 bitri [˙A / x]˙ B = C D = E