Metamath Proof Explorer

Theorem elxp6

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 . (Contributed by NM, 9-Oct-2004)

		Ref	Expression
	Assertion	elxp6	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨1^{st} (A), 2^{nd} (A)⟩ \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$

Proof

Step	Hyp	Ref	Expression
1		elxp4	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩ \land (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C))$
2		1stval	$⊢ 1^{st} (A) = ⋃ dom \{A\}$
3		2ndval	$⊢ 2^{nd} (A) = ⋃ ran \{A\}$
4	2 3	opeq12i	$⊢ ⟨1^{st} (A), 2^{nd} (A)⟩ = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩$
5	4	eqeq2i	$⊢ A = ⟨1^{st} (A), 2^{nd} (A)⟩ \leftrightarrow A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩$
6	2	eleq1i	$⊢ 1^{st} (A) \in B \leftrightarrow ⋃ dom \{A\} \in B$
7	3	eleq1i	$⊢ 2^{nd} (A) \in C \leftrightarrow ⋃ ran \{A\} \in C$
8	6 7	anbi12i	$⊢ (1^{st} (A) \in B \land 2^{nd} (A) \in C) \leftrightarrow (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C)$
9	5 8	anbi12i	$⊢ (A = ⟨1^{st} (A), 2^{nd} (A)⟩ \land (1^{st} (A) \in B \land 2^{nd} (A) \in C)) \leftrightarrow (A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩ \land (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C))$
10	1 9	bitr4i	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨1^{st} (A), 2^{nd} (A)⟩ \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$