Metamath Proof Explorer


Theorem relssdmrn

Description: A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of Mendelson p. 235. (Contributed by NM, 3-Aug-1994) (Proof shortened by SN, 23-Dec-2024)

Ref Expression
Assertion relssdmrn Rel A A dom A × ran A

Proof

Step Hyp Ref Expression
1 id Rel A Rel A
2 vex x V
3 vex y V
4 2 3 opeldm x y A x dom A
5 2 3 opelrn x y A y ran A
6 4 5 opelxpd x y A x y dom A × ran A
7 6 a1i Rel A x y A x y dom A × ran A
8 1 7 relssdv Rel A A dom A × ran A