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

Metamath Proof Explorer

Theorem elmptima

Description: The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion elmptima 
|- ( C e. V -> ( C e. ( ( x e. A |-> B ) " D ) <-> E. x e. ( A i^i D ) C = B ) )

Proof

Step Hyp Ref Expression
1 mptima 
 |-  ( ( x e. A |-> B ) " D ) = ran ( x e. ( A i^i D ) |-> B )
2 1 a1i 
 |-  ( C e. V -> ( ( x e. A |-> B ) " D ) = ran ( x e. ( A i^i D ) |-> B ) )
3 2 eleq2d 
 |-  ( C e. V -> ( C e. ( ( x e. A |-> B ) " D ) <-> C e. ran ( x e. ( A i^i D ) |-> B ) ) )
4 eqid 
 |-  ( x e. ( A i^i D ) |-> B ) = ( x e. ( A i^i D ) |-> B )
5 4 elrnmpt 
 |-  ( C e. V -> ( C e. ran ( x e. ( A i^i D ) |-> B ) <-> E. x e. ( A i^i D ) C = B ) )
6 3 5 bitrd 
 |-  ( C e. V -> ( C e. ( ( x e. A |-> B ) " D ) <-> E. x e. ( A i^i D ) C = B ) )