Metamath Proof Explorer


Theorem dfcnvrefrel3

Description: Alternate definition of the converse reflexive relation predicate. A relation is converse reflexive iff: for all elements on its domain and range, if for an element of its domain and for an element of its range there is the relation between them, then the two elements are the same, cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 25-Jul-2021)

Ref Expression
Assertion dfcnvrefrel3
|- ( CnvRefRel R <-> ( A. x e. dom R A. y e. ran R ( x R y -> x = y ) /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 df-cnvrefrel
 |-  ( CnvRefRel R <-> ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) )
2 inxpssidinxp
 |-  ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) <-> A. x e. dom R A. y e. ran R ( x R y -> x = y ) )
3 2 anbi1i
 |-  ( ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) <-> ( A. x e. dom R A. y e. ran R ( x R y -> x = y ) /\ Rel R ) )
4 1 3 bitri
 |-  ( CnvRefRel R <-> ( A. x e. dom R A. y e. ran R ( x R y -> x = y ) /\ Rel R ) )