elsnxp

Description: Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020) (Proof shortened by JJ, 14-Jul-2021)

		Ref	Expression
	Assertion	elsnxp	$⊢ X \in V \to (Z \in (\{X\} \times A) \leftrightarrow \exists y \in A Z = ⟨X, y⟩)$

Proof

Step	Hyp	Ref	Expression
1		elxp	$⊢ Z \in (\{X\} \times A) \leftrightarrow \exists x \exists y (Z = ⟨x, y⟩ \land (x \in \{X\} \land y \in A))$
2		df-rex	$⊢ \exists y \in A (x \in \{X\} \land Z = ⟨x, y⟩) \leftrightarrow \exists y (y \in A \land (x \in \{X\} \land Z = ⟨x, y⟩))$
3		an13	$⊢ (Z = ⟨x, y⟩ \land (x \in \{X\} \land y \in A)) \leftrightarrow (y \in A \land (x \in \{X\} \land Z = ⟨x, y⟩))$
4	3	exbii	$⊢ \exists y (Z = ⟨x, y⟩ \land (x \in \{X\} \land y \in A)) \leftrightarrow \exists y (y \in A \land (x \in \{X\} \land Z = ⟨x, y⟩))$
5	2 4	bitr4i	$⊢ \exists y \in A (x \in \{X\} \land Z = ⟨x, y⟩) \leftrightarrow \exists y (Z = ⟨x, y⟩ \land (x \in \{X\} \land y \in A))$
6		elsni	$⊢ x \in \{X\} \to x = X$
7	6	opeq1d	$⊢ x \in \{X\} \to ⟨x, y⟩ = ⟨X, y⟩$
8	7	eqeq2d	$⊢ x \in \{X\} \to (Z = ⟨x, y⟩ \leftrightarrow Z = ⟨X, y⟩)$
9	8	biimpa	$⊢ (x \in \{X\} \land Z = ⟨x, y⟩) \to Z = ⟨X, y⟩$
10	9	reximi	$⊢ \exists y \in A (x \in \{X\} \land Z = ⟨x, y⟩) \to \exists y \in A Z = ⟨X, y⟩$
11	5 10	sylbir	$⊢ \exists y (Z = ⟨x, y⟩ \land (x \in \{X\} \land y \in A)) \to \exists y \in A Z = ⟨X, y⟩$
12	11	exlimiv	$⊢ \exists x \exists y (Z = ⟨x, y⟩ \land (x \in \{X\} \land y \in A)) \to \exists y \in A Z = ⟨X, y⟩$
13	1 12	sylbi	$⊢ Z \in (\{X\} \times A) \to \exists y \in A Z = ⟨X, y⟩$
14		snidg	$⊢ X \in V \to X \in \{X\}$
15		opelxpi	$⊢ (X \in \{X\} \land y \in A) \to ⟨X, y⟩ \in (\{X\} \times A)$
16	14 15	sylan	$⊢ (X \in V \land y \in A) \to ⟨X, y⟩ \in (\{X\} \times A)$
17		eleq1	$⊢ Z = ⟨X, y⟩ \to (Z \in (\{X\} \times A) \leftrightarrow ⟨X, y⟩ \in (\{X\} \times A))$
18	16 17	syl5ibrcom	$⊢ (X \in V \land y \in A) \to (Z = ⟨X, y⟩ \to Z \in (\{X\} \times A))$
19	18	rexlimdva	$⊢ X \in V \to (\exists y \in A Z = ⟨X, y⟩ \to Z \in (\{X\} \times A))$
20	13 19	impbid2	$⊢ X \in V \to (Z \in (\{X\} \times A) \leftrightarrow \exists y \in A Z = ⟨X, y⟩)$

Metamath Proof Explorer

Theorem elsnxp

Proof