elin

Description: Expansion of membership in an intersection of two classes. Theorem 12 of Suppes p. 25. (Contributed by NM, 29-Apr-1994)

		Ref	Expression
	Assertion	elin	$⊢ A \in (B \cap C) \leftrightarrow (A \in B \land A \in C)$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in (B \cap C) \to A \in V$
2		elex	$⊢ A \in C \to A \in V$
3	2	adantl	$⊢ (A \in B \land A \in C) \to A \in V$
4		eleq1	$⊢ x = A \to (x \in B \leftrightarrow A \in B)$
5		eleq1	$⊢ x = A \to (x \in C \leftrightarrow A \in C)$
6	4 5	anbi12d	$⊢ x = A \to ((x \in B \land x \in C) \leftrightarrow (A \in B \land A \in C))$
7		df-in	$⊢ B \cap C = \{x \| (x \in B \land x \in C)\}$
8	6 7	elab2g	$⊢ A \in V \to (A \in (B \cap C) \leftrightarrow (A \in B \land A \in C))$
9	1 3 8	pm5.21nii	$⊢ A \in (B \cap C) \leftrightarrow (A \in B \land A \in C)$

Metamath Proof Explorer