Theorem elopabr

Description: Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021)

	Ref	Expression
Assertion	elopabr	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } → 𝐴 ∈ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		elopab	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )
2		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
3	2	biimpi	⊢ ( 𝑥 𝑅 𝑦 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
4		eleq1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
5	3 4	syl5ibr	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑥 𝑅 𝑦 → 𝐴 ∈ 𝑅 ) )
6	5	imp	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ∈ 𝑅 )
7	6	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ∈ 𝑅 )
8	1 7	sylbi	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } → 𝐴 ∈ 𝑅 )