Metamath Proof Explorer

Theorem dfcnvrefrel4

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

		Ref	Expression
	Assertion	dfcnvrefrel4	\|- ( CnvRefRel R <-> ( R C_ _I /\ Rel R ) )

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		cnvref4	\|- ( Rel R -> ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) <-> R C_ _I ) )
3	1 2	bianim	\|- ( CnvRefRel R <-> ( R C_ _I /\ Rel R ) )

Step

Hyp

Ref

Expression

 |-  ( CnvRefRel R <-> ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) /\ Rel R ) )

 |-  ( Rel R -> ( ( R i^i ( dom R X. ran R ) ) C_ ( _I i^i ( dom R X. ran R ) ) <-> R C_ _I ) )

1 2

 |-  ( CnvRefRel R <-> ( R C_ _I /\ Rel R ) )