Metamath Proof Explorer


Theorem dfss

Description: Variant of subclass definition df-ss . (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion dfss A B A = A B

Proof

Step Hyp Ref Expression
1 df-ss A B A B = A
2 eqcom A B = A A = A B
3 1 2 bitri A B A = A B