Metamath Proof Explorer


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 𝑅 → ( 𝑅 “ { 𝐴 } ) = { 𝑦𝐴 𝑅 𝑦 } )