Metamath Proof Explorer

Theorem relbrcnv

Description: When R is a relation, the sethood assumptions on brcnv can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypothesis relbrcnv.1 
|- Rel R
Assertion relbrcnv 
|- ( A `' R B <-> B R A )

Proof

Step Hyp Ref Expression
1 relbrcnv.1 
 |-  Rel R
2 relbrcnvg 
 |-  ( Rel R -> ( A `' R B <-> B R A ) )
3 1 2 ax-mp 
 |-  ( A `' R B <-> B R A )