Metamath Proof Explorer

Theorem elxp8

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 . (Contributed by ML, 19-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		xp1st	$⊢ A \in (B \times C) \to 1^{st} (A) \in B$
2		ssv	$⊢ B \subseteq V$
3		ssid	$⊢ C \subseteq C$
4		xpss12	$⊢ (B \subseteq V \land C \subseteq C) \to B \times C \subseteq V \times C$
5	2 3 4	mp2an	$⊢ B \times C \subseteq V \times C$
6	5	sseli	$⊢ A \in (B \times C) \to A \in (V \times C)$
7	1 6	jca	$⊢ A \in (B \times C) \to (1^{st} (A) \in B \land A \in (V \times C))$
8		xpss	$⊢ V \times C \subseteq V \times V$
9	8	sseli	$⊢ A \in (V \times C) \to A \in (V \times V)$
10	9	adantl	$⊢ (1^{st} (A) \in B \land A \in (V \times C)) \to A \in (V \times V)$
11		xp2nd	$⊢ A \in (V \times C) \to 2^{nd} (A) \in C$
12	11	anim2i	$⊢ (1^{st} (A) \in B \land A \in (V \times C)) \to (1^{st} (A) \in B \land 2^{nd} (A) \in C)$
13		elxp7	$⊢ A \in (B \times C) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$
14	10 12 13	sylanbrc	$⊢ (1^{st} (A) \in B \land A \in (V \times C)) \to A \in (B \times C)$
15	7 14	impbii	$⊢ A \in (B \times C) \leftrightarrow (1^{st} (A) \in B \land A \in (V \times C))$