Theorem relimasn

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

	Ref	Expression
Assertion	relimasn	⊢ ( Rel 𝑅 → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
2		imaeq2	⊢ ( { 𝐴 } = ∅ → ( 𝑅 “ { 𝐴 } ) = ( 𝑅 “ ∅ ) )
3	1 2	sylbi	⊢ ( ¬ 𝐴 ∈ V → ( 𝑅 “ { 𝐴 } ) = ( 𝑅 “ ∅ ) )
4		ima0	⊢ ( 𝑅 “ ∅ ) = ∅
5	3 4	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ( 𝑅 “ { 𝐴 } ) = ∅ )
6	5	adantl	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ( 𝑅 “ { 𝐴 } ) = ∅ )
7		brrelex1	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝑦 ) → 𝐴 ∈ V )
8	7	stoic1a	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ¬ 𝐴 𝑅 𝑦 )
9	8	nexdv	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ¬ ∃ 𝑦 𝐴 𝑅 𝑦 )
10		abn0	⊢ ( { 𝑦 ∣ 𝐴 𝑅 𝑦 } ≠ ∅ ↔ ∃ 𝑦 𝐴 𝑅 𝑦 )
11	10	necon1bbii	⊢ ( ¬ ∃ 𝑦 𝐴 𝑅 𝑦 ↔ { 𝑦 ∣ 𝐴 𝑅 𝑦 } = ∅ )
12	9 11	sylib	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → { 𝑦 ∣ 𝐴 𝑅 𝑦 } = ∅ )
13	6 12	eqtr4d	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )
14	13	ex	⊢ ( Rel 𝑅 → ( ¬ 𝐴 ∈ V → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } ) )
15		imasng	⊢ ( 𝐴 ∈ V → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )
16	14 15	pm2.61d2	⊢ ( Rel 𝑅 → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )