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 e. ( _V X. _V ) |-> <. ( 2nd ` x ) , ( 1st ` x ) >. )
Assertion elcnvlem 
|- ( A e. `' B <-> ( A e. ( _V X. _V ) /\ ( F ` A ) e. B ) )

Proof

Step Hyp Ref Expression
1 elcnvlem.f 
 |-  F = ( x e. ( _V X. _V ) |-> <. ( 2nd ` x ) , ( 1st ` x ) >. )
2 elcnv2 
 |-  ( A e. `' B <-> E. u E. v ( A = <. u , v >. /\ <. v , u >. e. B ) )
3 fveq2 
 |-  ( A = <. u , v >. -> ( F ` A ) = ( F ` <. u , v >. ) )
4 vex 
 |-  u e. _V
5 vex 
 |-  v e. _V
6 4 5 opelvv 
 |-  <. u , v >. e. ( _V X. _V )
7 4 5 op2ndd 
 |-  ( x = <. u , v >. -> ( 2nd ` x ) = v )
8 4 5 op1std 
 |-  ( x = <. u , v >. -> ( 1st ` x ) = u )
9 7 8 opeq12d 
 |-  ( x = <. u , v >. -> <. ( 2nd ` x ) , ( 1st ` x ) >. = <. v , u >. )
10 opex 
 |-  <. v , u >. e. _V
11 9 1 10 fvmpt 
 |-  ( <. u , v >. e. ( _V X. _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 ) e. B <-> <. v , u >. e. B ) )
15 14 copsex2gb 
 |-  ( E. u E. v ( A = <. u , v >. /\ <. v , u >. e. B ) <-> ( A e. ( _V X. _V ) /\ ( F ` A ) e. B ) )
16 2 15 bitri 
 |-  ( A e. `' B <-> ( A e. ( _V X. _V ) /\ ( F ` A ) e. B ) )