Theorem imasng

Description: The image of a singleton. (Contributed by NM, 8-May-2005)

	Ref	Expression
Assertion	imasng	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
2		dfima2	⊢ ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑥 𝑅 𝑦 }
3		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝑦 ) )
4	3	rexsng	⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 ∈ { 𝐴 } 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝑦 ) )
5	4	abbidv	⊢ ( 𝐴 ∈ V → { 𝑦 ∣ ∃ 𝑥 ∈ { 𝐴 } 𝑥 𝑅 𝑦 } = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )
6	2 5	eqtrid	⊢ ( 𝐴 ∈ V → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )
7	1 6	syl	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )