Description: Equality of a class variable and a class abstraction. Commuted form of eqabb . (Contributed by NM, 20-Aug-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | eqabcb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqabb | ||
2 | eqcom | ||
3 | bicom | ||
4 | 3 | albii | |
5 | 1 2 4 | 3bitr4i |