Metamath Proof Explorer

Theorem elxp7

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

		Ref	Expression
	Assertion	elxp7	$⊢ A \in (B \times C) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$

Proof

Step	Hyp	Ref	Expression
1		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))$
2		fvex	$⊢ 1^{st} (A) \in V$
3		fvex	$⊢ 2^{nd} (A) \in V$
4	2 3	pm3.2i	$⊢ (1^{st} (A) \in V \land 2^{nd} (A) \in V)$
5		elxp6	$⊢ A \in (V \times V) \leftrightarrow (A = ⟨1^{st} (A), 2^{nd} (A)⟩ \land (1^{st} (A) \in V \land 2^{nd} (A) \in V))$
6	4 5	mpbiran2	$⊢ A \in (V \times V) \leftrightarrow A = ⟨1^{st} (A), 2^{nd} (A)⟩$
7	6	anbi1i	$⊢ (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C)) \leftrightarrow (A = ⟨1^{st} (A), 2^{nd} (A)⟩ \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$
8	1 7	bitr4i	$⊢ A \in (B \times C) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$