Metamath Proof Explorer

Theorem dfcnvrefrel5

Description: Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024)

Ref Expression
Assertion dfcnvrefrel5 
|- ( CnvRefRel R <-> ( A. x A. y ( x R y -> x = y ) /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 dfcnvrefrel4 
 |-  ( CnvRefRel R <-> ( R C_ _I /\ Rel R ) )
2 cnvref5 
 |-  ( Rel R -> ( R C_ _I <-> A. x A. y ( x R y -> x = y ) ) )
3 1 2 bianim 
 |-  ( CnvRefRel R <-> ( A. x A. y ( x R y -> x = y ) /\ Rel R ) )