Theorem 1st2ndbr

Description: Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016)

	Ref	Expression
Assertion	1st2ndbr	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to 1^{st}\left(A\right)B{2}^{nd}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		1st2nd	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
2		simpr	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to A\in B$$
3	1 2	eqeltrrd	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in B$$
4		df-br	$$⊢1^{st}\left(A\right)B{2}^{nd}\left(A\right)\leftrightarrow ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in B$$
5	3 4	sylibr	$$⊢\left(\mathrm{Rel}B\wedge A\in B\right)\to 1^{st}\left(A\right)B{2}^{nd}\left(A\right)$$