Metamath Proof Explorer


Theorem elcnvintab

Description: Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020)

Ref Expression
Assertion elcnvintab A x | φ -1 A V × V x φ A x -1

Proof

Step Hyp Ref Expression
1 eqid y V × V 2 nd y 1 st y = y V × V 2 nd y 1 st y
2 1 elcnvlem A x | φ -1 A V × V y V × V 2 nd y 1 st y A x | φ
3 1 elcnvlem A x -1 A V × V y V × V 2 nd y 1 st y A x
4 2 3 elmapintab A x | φ -1 A V × V x φ A x -1