Metamath Proof Explorer


Theorem dfss

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

Ref Expression
Assertion dfss ( 𝐴𝐵𝐴 = ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-ss ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = 𝐴 )
2 eqcom ( ( 𝐴𝐵 ) = 𝐴𝐴 = ( 𝐴𝐵 ) )
3 1 2 bitri ( 𝐴𝐵𝐴 = ( 𝐴𝐵 ) )