Metamath Proof Explorer


Theorem relimasn

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

Ref Expression
Assertion relimasn Rel R R A = y | A R y

Proof

Step Hyp Ref Expression
1 snprc ¬ A V A =
2 imaeq2 A = R A = R
3 1 2 sylbi ¬ A V R A = R
4 ima0 R =
5 3 4 eqtrdi ¬ A V R A =
6 5 adantl Rel R ¬ A V R A =
7 brrelex1 Rel R A R y A V
8 7 stoic1a Rel R ¬ A V ¬ A R y
9 8 nexdv Rel R ¬ A V ¬ y A R y
10 abn0 y | A R y y A R y
11 10 necon1bbii ¬ y A R y y | A R y =
12 9 11 sylib Rel R ¬ A V y | A R y =
13 6 12 eqtr4d Rel R ¬ A V R A = y | A R y
14 13 ex Rel R ¬ A V R A = y | A R y
15 imasng A V R A = y | A R y
16 14 15 pm2.61d2 Rel R R A = y | A R y