Theorem dfss2 3237

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of [TakeutiZaring] p. 18. This is another name for df-ss 3233 which is more consistent with the naming in the Metamath Proof Explorer. (Contributed by NM, 27-Apr-1994.)

Assertion

Ref	Expression
dfss2	|- ( A C_ B <-> ( A i^i B ) = A )

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		df-ss 3233	1 |- ( A C_ B <-> ( A i^i B ) = A )

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   i^i cin 3219   C_ wss 3220

This proof depends on definitions:  df-ss 3233

This theorem is used by:  bitsinv1  12729  ballotfilemfp1  13231  trlsegvdeglem6  16706