Metamath Proof Explorer

Theorem elcnv

Description: Membership in a converse relation. Equation 5 of Suppes p. 62. (Contributed by NM, 24-Mar-1998)

Ref Expression
Assertion elcnv 
|- ( A e. `' R <-> E. x E. y ( A = <. x , y >. /\ y R x ) )

Proof

Step Hyp Ref Expression
1 df-cnv 
 |-  `' R = { <. x , y >. | y R x }
2 1 eleq2i 
 |-  ( A e. `' R <-> A e. { <. x , y >. | y R x } )
3 elopab 
 |-  ( A e. { <. x , y >. | y R x } <-> E. x E. y ( A = <. x , y >. /\ y R x ) )
4 2 3 bitri 
 |-  ( A e. `' R <-> E. x E. y ( A = <. x , y >. /\ y R x ) )