elin3

Description: Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015)

		Ref	Expression
	Hypothesis	elin3.x	$⊢ X = (B \cap C) \cap D$
	Assertion	elin3	$⊢ A \in X \leftrightarrow (A \in B \land A \in C \land A \in D)$

Step	Hyp	Ref	Expression
1		elin3.x	$⊢ X = (B \cap C) \cap D$
2		elin	$⊢ A \in (B \cap C) \leftrightarrow (A \in B \land A \in C)$
3	2	anbi1i	$⊢ (A \in (B \cap C) \land A \in D) \leftrightarrow ((A \in B \land A \in C) \land A \in D)$
4	1	elin2	$⊢ A \in X \leftrightarrow (A \in (B \cap C) \land A \in D)$
5		df-3an	$⊢ (A \in B \land A \in C \land A \in D) \leftrightarrow ((A \in B \land A \in C) \land A \in D)$
6	3 4 5	3bitr4i	$⊢ A \in X \leftrightarrow (A \in B \land A \in C \land A \in D)$

Metamath Proof Explorer