Metamath Proof Explorer

Theorem dfss2OLD

Description: Obsolete version of dfss2 as of 16-May-2024. (Contributed by NM, 8-Jan-2002) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dfss	$⊢ A \subseteq B \leftrightarrow A = A \cap B$
2		df-in	$⊢ A \cap B = \{x \| (x \in A \land x \in B)\}$
3	2	eqeq2i	$⊢ A = A \cap B \leftrightarrow A = \{x \| (x \in A \land x \in B)\}$
4		eqabb	$⊢ A = \{x \| (x \in A \land x \in B)\} \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land x \in B))$
5	1 3 4	3bitri	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land x \in B))$
6		pm4.71	$⊢ (x \in A \to x \in B) \leftrightarrow (x \in A \leftrightarrow (x \in A \land x \in B))$
7	6	albii	$⊢ \forall x (x \in A \to x \in B) \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land x \in B))$
8	5 7	bitr4i	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$