elrelb

Description: A member of a relation expressed by an ordered pair. (Contributed by AV, 23-Aug-2026)

		Ref	Expression
	Assertion	elrelb	$⊢ Rel R \to (A \in R \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land x R y))$

Step	Hyp	Ref	Expression
1		elrel	$⊢ (Rel R \land A \in R) \to \exists x \exists y A = ⟨x, y⟩$
2		eleq1	$⊢ A = ⟨x, y⟩ \to (A \in R \leftrightarrow ⟨x, y⟩ \in R)$
3		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
4	3	biimpri	$⊢ ⟨x, y⟩ \in R \to x R y$
5	2 4	biimtrdi	$⊢ A = ⟨x, y⟩ \to (A \in R \to x R y)$
6	5	com12	$⊢ A \in R \to (A = ⟨x, y⟩ \to x R y)$
7	6	adantl	$⊢ (Rel R \land A \in R) \to (A = ⟨x, y⟩ \to x R y)$
8	7	ancld	$⊢ (Rel R \land A \in R) \to (A = ⟨x, y⟩ \to (A = ⟨x, y⟩ \land x R y))$
9	8	2eximdv	$⊢ (Rel R \land A \in R) \to (\exists x \exists y A = ⟨x, y⟩ \to \exists x \exists y (A = ⟨x, y⟩ \land x R y))$
10	1 9	mpd	$⊢ (Rel R \land A \in R) \to \exists x \exists y (A = ⟨x, y⟩ \land x R y)$
11	10	ex	$⊢ Rel R \to (A \in R \to \exists x \exists y (A = ⟨x, y⟩ \land x R y))$
12	3	bilani	$⊢ (A = ⟨x, y⟩ \land x R y) \to ⟨x, y⟩ \in R$
13	2	adantr	$⊢ (A = ⟨x, y⟩ \land x R y) \to (A \in R \leftrightarrow ⟨x, y⟩ \in R)$
14	12 13	mpbird	$⊢ (A = ⟨x, y⟩ \land x R y) \to A \in R$
15	14	exlimiv	$⊢ \exists y (A = ⟨x, y⟩ \land x R y) \to A \in R$
16	15	exlimiv	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land x R y) \to A \in R$
17	11 16	impbid1	$⊢ Rel R \to (A \in R \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land x R y))$

Metamath Proof Explorer