Metamath Proof Explorer


Theorem elcnvlem

Description: Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020)

Ref Expression
Hypothesis elcnvlem.f F = x V × V 2 nd x 1 st x
Assertion elcnvlem A B -1 A V × V F A B

Proof

Step Hyp Ref Expression
1 elcnvlem.f F = x V × V 2 nd x 1 st x
2 elcnv2 A B -1 u v A = u v v u B
3 fveq2 A = u v F A = F u v
4 vex u V
5 vex v V
6 4 5 opelvv u v V × V
7 4 5 op2ndd x = u v 2 nd x = v
8 4 5 op1std x = u v 1 st x = u
9 7 8 opeq12d x = u v 2 nd x 1 st x = v u
10 opex v u V
11 9 1 10 fvmpt u v V × V F u v = v u
12 6 11 ax-mp F u v = v u
13 3 12 eqtrdi A = u v F A = v u
14 13 eleq1d A = u v F A B v u B
15 14 copsex2gb u v A = u v v u B A V × V F A B
16 2 15 bitri A B -1 A V × V F A B