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 i^i dom R ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- y e. _V
2		vex	|- x e. _V
3	1 2	breldm	|- ( y R x -> y e. dom R )
4	3	pm4.71ri	|- ( y R x <-> ( y e. dom R /\ y R x ) )
5	4	rexbii	|- ( E. y e. A y R x <-> E. y e. A ( y e. dom R /\ y R x ) )
6		rexin	|- ( E. y e. ( A i^i dom R ) y R x <-> E. y e. A ( y e. dom R /\ y R x ) )
7	5 6	bitr4i	|- ( E. y e. A y R x <-> E. y e. ( A i^i dom R ) y R x )
8	2	elima	|- ( x e. ( R " A ) <-> E. y e. A y R x )
9	2	elima	|- ( x e. ( R " ( A i^i dom R ) ) <-> E. y e. ( A i^i dom R ) y R x )
10	7 8 9	3bitr4i	|- ( x e. ( R " A ) <-> x e. ( R " ( A i^i dom R ) ) )
11	10	eqriv	|- ( R " A ) = ( R " ( A i^i dom R ) )