Metamath Proof Explorer

Theorem dfss2

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of TakeutiZaring p. 17. (Contributed by NM, 8-Jan-2002) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 16-May-2024)

		Ref	Expression
	Assertion	dfss2	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$⊢ A = A \cap B \leftrightarrow \forall x (x \in A \leftrightarrow x \in (A \cap B))$
2		dfss	$⊢ A \subseteq B \leftrightarrow A = A \cap B$
3		pm4.71	$⊢ (x \in A \to x \in B) \leftrightarrow (x \in A \leftrightarrow (x \in A \land x \in B))$
4		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
5	4	bibi2i	$⊢ (x \in A \leftrightarrow x \in (A \cap B)) \leftrightarrow (x \in A \leftrightarrow (x \in A \land x \in B))$
6	3 5	bitr4i	$⊢ (x \in A \to x \in B) \leftrightarrow (x \in A \leftrightarrow x \in (A \cap B))$
7	6	albii	$⊢ \forall x (x \in A \to x \in B) \leftrightarrow \forall x (x \in A \leftrightarrow x \in (A \cap B))$
8	1 2 7	3bitr4i	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$