Theorem dfss2 3227

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

Assertion

Ref	Expression
dfss2	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		df-ss 3223	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)

Syntax hints:   ↔ wb 105   = wceq 1398   ∩ cin 3209   ⊆ wss 3210

This theorem depends on definitions:  df-ss 3223

This theorem is referenced by:  bitsinv1  12644  trlsegvdeglem6  16452