Theorem cnvref5

Description: Two ways to say that a relation is a subclass of the identity relation. (Contributed by Peter Mazsa, 26-Jun-2019)

	Ref	Expression
Assertion	cnvref5	|- ( Rel R -> ( R C_ _I <-> A. x A. y ( x R y -> x = y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssrel3	|- ( Rel R -> ( R C_ _I <-> A. x A. y ( x R y -> x _I y ) ) )
2		ideqg	|- ( y e. _V -> ( x _I y <-> x = y ) )
3	2	elv	|- ( x _I y <-> x = y )
4	3	imbi2i	|- ( ( x R y -> x _I y ) <-> ( x R y -> x = y ) )
5	4	2albii	|- ( A. x A. y ( x R y -> x _I y ) <-> A. x A. y ( x R y -> x = y ) )
6	1 5	bitrdi	|- ( Rel R -> ( R C_ _I <-> A. x A. y ( x R y -> x = y ) ) )