dfss2

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of TakeutiZaring p. 18. This was the original definition before df-ss . (Contributed by NM, 27-Apr-1994) Revise df-ss . (Revised by GG, 15-May-2025)

		Ref	Expression
	Assertion	dfss2	$⊢ A \subseteq B \leftrightarrow A \cap B = A$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$⊢ \{y \| (y \in A \land y \in B)\} = A \leftrightarrow \forall x (x \in \{y \| (y \in A \land y \in B)\} \leftrightarrow x \in A)$
2		df-in	$⊢ A \cap B = \{y \| (y \in A \land y \in B)\}$
3	2	eqeq1i	$⊢ A \cap B = A \leftrightarrow \{y \| (y \in A \land y \in B)\} = A$
4		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
5		simp2	$⊢ ((x \in A \to x \in B) \land x \in A \land x \in B) \to x \in A$
6	5	3expib	$⊢ (x \in A \to x \in B) \to ((x \in A \land x \in B) \to x \in A)$
7		ancl	$⊢ (x \in A \to x \in B) \to (x \in A \to (x \in A \land x \in B))$
8	6 7	impbid	$⊢ (x \in A \to x \in B) \to ((x \in A \land x \in B) \leftrightarrow x \in A)$
9		dfbi2	$⊢ ((x \in A \land x \in B) \leftrightarrow x \in A) \leftrightarrow (((x \in A \land x \in B) \to x \in A) \land (x \in A \to (x \in A \land x \in B)))$
10		pm2.21	$⊢ \neg x \in A \to (x \in A \to x \in B)$
11		pm3.4	$⊢ (x \in A \land x \in B) \to (x \in A \to x \in B)$
12	10 11	ja	$⊢ (x \in A \to (x \in A \land x \in B)) \to (x \in A \to x \in B)$
13	9 12	simplbiim	$⊢ ((x \in A \land x \in B) \leftrightarrow x \in A) \to (x \in A \to x \in B)$
14	8 13	impbii	$⊢ (x \in A \to x \in B) \leftrightarrow ((x \in A \land x \in B) \leftrightarrow x \in A)$
15		df-clab	$⊢ x \in \{y \| (y \in A \land y \in B)\} \leftrightarrow [x/ y] (y \in A \land y \in B)$
16		eleq1w	$⊢ y = x \to (y \in A \leftrightarrow x \in A)$
17		eleq1w	$⊢ y = x \to (y \in B \leftrightarrow x \in B)$
18	16 17	anbi12d	$⊢ y = x \to ((y \in A \land y \in B) \leftrightarrow (x \in A \land x \in B))$
19	18	sbievw	$⊢ [x/ y] (y \in A \land y \in B) \leftrightarrow (x \in A \land x \in B)$
20	15 19	bitr2i	$⊢ (x \in A \land x \in B) \leftrightarrow x \in \{y \| (y \in A \land y \in B)\}$
21	20	bibi1i	$⊢ ((x \in A \land x \in B) \leftrightarrow x \in A) \leftrightarrow (x \in \{y \| (y \in A \land y \in B)\} \leftrightarrow x \in A)$
22	14 21	bitri	$⊢ (x \in A \to x \in B) \leftrightarrow (x \in \{y \| (y \in A \land y \in B)\} \leftrightarrow x \in A)$
23	22	albii	$⊢ \forall x (x \in A \to x \in B) \leftrightarrow \forall x (x \in \{y \| (y \in A \land y \in B)\} \leftrightarrow x \in A)$
24	4 23	bitri	$⊢ A \subseteq B \leftrightarrow \forall x (x \in \{y \| (y \in A \land y \in B)\} \leftrightarrow x \in A)$
25	1 3 24	3bitr4ri	$⊢ A \subseteq B \leftrightarrow A \cap B = A$

Metamath Proof Explorer

Theorem dfss2

Proof