Metamath Proof Explorer


Theorem intimasn2

Description: Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion intimasn2 B V A B = x A x B

Proof

Step Hyp Ref Expression
1 intimasn B V A B = y | x A y = x B
2 intima0 x A x B = y | x A y = x B
3 1 2 eqtr4di B V A B = x A x B