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 𝑅
Assertion relbrcnv ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐴 )

Proof

Step Hyp Ref Expression
1 relbrcnv.1 Rel 𝑅
2 relbrcnvg ( Rel 𝑅 → ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐴 ) )
3 1 2 ax-mp ( 𝐴 𝑅 𝐵𝐵 𝑅 𝐴 )