Theorem dfantisymrel4

Description: Alternate definition of the antisymmetric relation predicate. (Contributed by Peter Mazsa, 24-Jun-2024)

	Ref	Expression
Assertion	dfantisymrel4	|- ( AntisymRel R <-> ( ( R i^i `' R ) C_ _I /\ Rel R ) )

Proof

Step	Hyp	Ref	Expression
1		df-antisymrel	|- ( AntisymRel R <-> ( CnvRefRel ( R i^i `' R ) /\ Rel R ) )
2		relcnv	|- Rel `' R
3		relin2	|- ( Rel `' R -> Rel ( R i^i `' R ) )
4	2 3	ax-mp	|- Rel ( R i^i `' R )
5		dfcnvrefrel4	|- ( CnvRefRel ( R i^i `' R ) <-> ( ( R i^i `' R ) C_ _I /\ Rel ( R i^i `' R ) ) )
6	4 5	mpbiran2	|- ( CnvRefRel ( R i^i `' R ) <-> ( R i^i `' R ) C_ _I )
7	1 6	bianbi	|- ( AntisymRel R <-> ( ( R i^i `' R ) C_ _I /\ Rel R ) )