Description: Variant of subclass definition dfss . (Contributed by NM, 21Jun1993)
Ref  Expression  

Assertion  dfss   ( A C_ B <> A = ( A i^i B ) ) 
Step  Hyp  Ref  Expression 

1  dfss   ( A C_ B <> ( A i^i B ) = A ) 

2  eqcom   ( ( A i^i B ) = A <> A = ( A i^i B ) ) 

3  1 2  bitri   ( A C_ B <> A = ( A i^i B ) ) 