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 𝑎𝐴 ( 𝑎𝐵 ) = { 𝑥 ∣ ∃ 𝑎𝐴 𝑥 = ( 𝑎𝐵 ) }

Proof

Step Hyp Ref Expression
1 vex 𝑎 ∈ V
2 1 imaex ( 𝑎𝐵 ) ∈ V
3 2 dfiin2 𝑎𝐴 ( 𝑎𝐵 ) = { 𝑥 ∣ ∃ 𝑎𝐴 𝑥 = ( 𝑎𝐵 ) }