Metamath Proof Explorer

Theorem intima0

Description: Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion intima0 
|- |^|_ a e. A ( a " B ) = |^| { x | E. a e. A x = ( a " B ) }

Proof

Step Hyp Ref Expression
1 vex 
 |-  a e. _V
2 1 imaex 
 |-  ( a " B ) e. _V
3 2 dfiin2 
 |-  |^|_ a e. A ( a " B ) = |^| { x | E. a e. A x = ( a " B ) }