Theorem 2ndrn

Description: The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	2ndrn	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( 2nd ‘ 𝐴 ) ∈ ran 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		1st2nd	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
2		simpr	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → 𝐴 ∈ 𝑅 )
3	1 2	eqeltrrd	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ∈ 𝑅 )
4		fvex	⊢ ( 1st ‘ 𝐴 ) ∈ V
5		fvex	⊢ ( 2nd ‘ 𝐴 ) ∈ V
6	4 5	opelrn	⊢ ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ∈ 𝑅 → ( 2nd ‘ 𝐴 ) ∈ ran 𝑅 )
7	3 6	syl	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( 2nd ‘ 𝐴 ) ∈ ran 𝑅 )