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

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 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 ) )