Metamath Proof Explorer

Theorem sseqin2

Description: A relationship between subclass and intersection. Similar to Exercise 9 of TakeutiZaring p. 18. (Contributed by NM, 17-May-1994)

Ref Expression
Assertion sseqin2 A B B A = A


Step Hyp Ref Expression
1 df-ss A B A B = A
2 incom A B = B A
3 2 eqeq1i A B = A B A = A
4 1 3 bitri A B B A = A