This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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