Theorem elrelb

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

	Ref	Expression
Assertion	elrelb	⊢ ( Rel 𝑅 → ( 𝐴 ∈ 𝑅 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elrel	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2		eleq1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
3		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
4	3	biimpri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → 𝑥 𝑅 𝑦 )
5	2 4	biimtrdi	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝑅 → 𝑥 𝑅 𝑦 ) )
6	5	com12	⊢ ( 𝐴 ∈ 𝑅 → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑥 𝑅 𝑦 ) )
7	6	adantl	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑥 𝑅 𝑦 ) )
8	7	ancld	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )
9	8	2eximdv	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )
10	1 9	mpd	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )
11	10	ex	⊢ ( Rel 𝑅 → ( 𝐴 ∈ 𝑅 → ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )
12	3	bilani	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
13	2	adantr	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → ( 𝐴 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
14	12 13	mpbird	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ∈ 𝑅 )
15	14	exlimiv	⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ∈ 𝑅 )
16	15	exlimiv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ∈ 𝑅 )
17	11 16	impbid1	⊢ ( Rel 𝑅 → ( 𝐴 ∈ 𝑅 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )