Theorem rnsnopg

Description: The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	rnsnopg	⊢ ( 𝐴 ∈ 𝑉 → ran { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran { ⟨ 𝐴 , 𝐵 ⟩ } = dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ }
2		dfdm4	⊢ dom { ⟨ 𝐵 , 𝐴 ⟩ } = ran ◡ { ⟨ 𝐵 , 𝐴 ⟩ }
3		df-rn	⊢ ran ◡ { ⟨ 𝐵 , 𝐴 ⟩ } = dom ◡ ◡ { ⟨ 𝐵 , 𝐴 ⟩ }
4		cnvcnvsn	⊢ ◡ ◡ { ⟨ 𝐵 , 𝐴 ⟩ } = ◡ { ⟨ 𝐴 , 𝐵 ⟩ }
5	4	dmeqi	⊢ dom ◡ ◡ { ⟨ 𝐵 , 𝐴 ⟩ } = dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ }
6	2 3 5	3eqtri	⊢ dom { ⟨ 𝐵 , 𝐴 ⟩ } = dom ◡ { ⟨ 𝐴 , 𝐵 ⟩ }
7	1 6	eqtr4i	⊢ ran { ⟨ 𝐴 , 𝐵 ⟩ } = dom { ⟨ 𝐵 , 𝐴 ⟩ }
8		dmsnopg	⊢ ( 𝐴 ∈ 𝑉 → dom { ⟨ 𝐵 , 𝐴 ⟩ } = { 𝐵 } )
9	7 8	syl5eq	⊢ ( 𝐴 ∈ 𝑉 → ran { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐵 } )