Metamath Proof Explorer


Theorem imaindm

Description: The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021)

Ref Expression
Assertion imaindm R A = R A dom R

Proof

Step Hyp Ref Expression
1 vex y V
2 vex x V
3 1 2 breldm y R x y dom R
4 3 pm4.71ri y R x y dom R y R x
5 4 rexbii y A y R x y A y dom R y R x
6 rexin y A dom R y R x y A y dom R y R x
7 5 6 bitr4i y A y R x y A dom R y R x
8 2 elima x R A y A y R x
9 2 elima x R A dom R y A dom R y R x
10 7 8 9 3bitr4i x R A x R A dom R
11 10 eqriv R A = R A dom R