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	alrimiv	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ∀ 𝑥 ¬ 𝐴 𝑅 𝑥 )
10		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝐴 𝑅 𝑦 ↔ 𝐴 𝑅 𝑥 ) )
11	10	ab0w	⊢ ( { 𝑦 ∣ 𝐴 𝑅 𝑦 } = ∅ ↔ ∀ 𝑥 ¬ 𝐴 𝑅 𝑥 )
12	9 11	sylibr	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → { 𝑦 ∣ 𝐴 𝑅 𝑦 } = ∅ )
13	6 12	eqtr4d	⊢ ( ( Rel 𝑅 ∧ ¬ 𝐴 ∈ V ) → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )
14	13	ex	⊢ ( Rel 𝑅 → ( ¬ 𝐴 ∈ V → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } ) )
15		imasng	⊢ ( 𝐴 ∈ V → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )
16	14 15	pm2.61d2	⊢ ( Rel 𝑅 → ( 𝑅 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝑅 𝑦 } )