elidinxp

Description: Characterization of the elements of the intersection of the identity relation with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022)

		Ref	Expression
	Assertion	elidinxp	$⊢ C \in (I \cap (A \times B)) \leftrightarrow \exists x \in (A \cap B) C = ⟨x, x⟩$

Proof

Step	Hyp	Ref	Expression
1		risset	$⊢ x \in B \leftrightarrow \exists y \in B y = x$
2	1	anbi2ci	$⊢ (x \in B \land C = ⟨x, x⟩) \leftrightarrow (C = ⟨x, x⟩ \land \exists y \in B y = x)$
3		r19.42v	$⊢ \exists y \in B (C = ⟨x, x⟩ \land y = x) \leftrightarrow (C = ⟨x, x⟩ \land \exists y \in B y = x)$
4		opeq2	$⊢ x = y \to ⟨x, x⟩ = ⟨x, y⟩$
5	4	equcoms	$⊢ y = x \to ⟨x, x⟩ = ⟨x, y⟩$
6	5	eqeq2d	$⊢ y = x \to (C = ⟨x, x⟩ \leftrightarrow C = ⟨x, y⟩)$
7	6	pm5.32ri	$⊢ (C = ⟨x, x⟩ \land y = x) \leftrightarrow (C = ⟨x, y⟩ \land y = x)$
8		vex	$⊢ y \in V$
9	8	ideq	$⊢ x I y \leftrightarrow x = y$
10		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
11		equcom	$⊢ x = y \leftrightarrow y = x$
12	9 10 11	3bitr3i	$⊢ ⟨x, y⟩ \in I \leftrightarrow y = x$
13	12	anbi2i	$⊢ (C = ⟨x, y⟩ \land ⟨x, y⟩ \in I) \leftrightarrow (C = ⟨x, y⟩ \land y = x)$
14	7 13	bitr4i	$⊢ (C = ⟨x, x⟩ \land y = x) \leftrightarrow (C = ⟨x, y⟩ \land ⟨x, y⟩ \in I)$
15	14	rexbii	$⊢ \exists y \in B (C = ⟨x, x⟩ \land y = x) \leftrightarrow \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in I)$
16	2 3 15	3bitr2i	$⊢ (x \in B \land C = ⟨x, x⟩) \leftrightarrow \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in I)$
17	16	rexbii	$⊢ \exists x \in A (x \in B \land C = ⟨x, x⟩) \leftrightarrow \exists x \in A \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in I)$
18		rexin	$⊢ \exists x \in (A \cap B) C = ⟨x, x⟩ \leftrightarrow \exists x \in A (x \in B \land C = ⟨x, x⟩)$
19		elinxp	$⊢ C \in (I \cap (A \times B)) \leftrightarrow \exists x \in A \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in I)$
20	17 18 19	3bitr4ri	$⊢ C \in (I \cap (A \times B)) \leftrightarrow \exists x \in (A \cap B) C = ⟨x, x⟩$

Metamath Proof Explorer

Theorem elidinxp

Proof