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	⊢ ( ( Rel 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 1^st ‘ 𝐴 ) 𝐵 ( 2^nd ‘ 𝐴 ) )

Step	Hyp	Ref	Expression
1		1st2nd	⊢ ( ( Rel 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
2		simpr	⊢ ( ( Rel 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
3	1 2	eqeltrrd	⊢ ( ( Rel 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∈ 𝐵 )
4		df-br	⊢ ( ( 1^st ‘ 𝐴 ) 𝐵 ( 2^nd ‘ 𝐴 ) ↔ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∈ 𝐵 )
5	3 4	sylibr	⊢ ( ( Rel 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 1^st ‘ 𝐴 ) 𝐵 ( 2^nd ‘ 𝐴 ) )

Metamath Proof Explorer