Metamath Proof Explorer

Theorem eliunxp

Description: Membership in a union of Cartesian products. Analogue of elxp for nonconstant B ( x ) . (Contributed by Mario Carneiro, 29-Dec-2014)

		Ref	Expression
	Assertion	eliunxp	$⊢ C \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \exists x \exists y (C = ⟨x, y⟩ \land (x \in A \land y \in B))$

Proof

Step	Hyp	Ref	Expression
1		relxp	$⊢ Rel (\{x\} \times B)$
2	1	rgenw	$⊢ \forall x \in A Rel (\{x\} \times B)$
3		reliun	$⊢ Rel ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \forall x \in A Rel (\{x\} \times B)$
4	2 3	mpbir	$⊢ Rel ⋃_{x \in A} (\{x\} \times B)$
5		elrel	$⊢ (Rel ⋃_{x \in A} (\{x\} \times B) \land C \in ⋃_{x \in A} (\{x\} \times B)) \to \exists x \exists y C = ⟨x, y⟩$
6	4 5	mpan	$⊢ C \in ⋃_{x \in A} (\{x\} \times B) \to \exists x \exists y C = ⟨x, y⟩$
7	6	pm4.71ri	$⊢ C \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow (\exists x \exists y C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B))$
8		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} (\{x\} \times B)$
9	8	nfel2	$⊢ Ⅎ x C \in ⋃_{x \in A} (\{x\} \times B)$
10	9	19.41	$⊢ \exists x (\exists y C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B)) \leftrightarrow (\exists x \exists y C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B))$
11		19.41v	$⊢ \exists y (C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B)) \leftrightarrow (\exists y C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B))$
12		eleq1	$⊢ C = ⟨x, y⟩ \to (C \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow ⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B))$
13		opeliunxp	$⊢ ⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow (x \in A \land y \in B)$
14	12 13	bitrdi	$⊢ C = ⟨x, y⟩ \to (C \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow (x \in A \land y \in B))$
15	14	pm5.32i	$⊢ (C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B)) \leftrightarrow (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
16	15	exbii	$⊢ \exists y (C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B)) \leftrightarrow \exists y (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
17	11 16	bitr3i	$⊢ (\exists y C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B)) \leftrightarrow \exists y (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
18	17	exbii	$⊢ \exists x (\exists y C = ⟨x, y⟩ \land C \in ⋃_{x \in A} (\{x\} \times B)) \leftrightarrow \exists x \exists y (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
19	7 10 18	3bitr2i	$⊢ C \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \exists x \exists y (C = ⟨x, y⟩ \land (x \in A \land y \in B))$