Theorem relexp2

Description: A set operated on by the relation exponent to the second power is equal to the composition of the set with itself. (Contributed by RP, 1-Jun-2020)

	Ref	Expression
Assertion	relexp2	|- ( R e. V -> ( R ^r 2 ) = ( R o. R ) )

Proof

Step	Hyp	Ref	Expression
1		df-2	|- 2 = ( 1 + 1 )
2	1	oveq2i	|- ( R ^r 2 ) = ( R ^r ( 1 + 1 ) )
3	2	a1i	|- ( R e. V -> ( R ^r 2 ) = ( R ^r ( 1 + 1 ) ) )
4		1nn	|- 1 e. NN
5		relexpsucnnr	|- ( ( R e. V /\ 1 e. NN ) -> ( R ^r ( 1 + 1 ) ) = ( ( R ^r 1 ) o. R ) )
6	4 5	mpan2	|- ( R e. V -> ( R ^r ( 1 + 1 ) ) = ( ( R ^r 1 ) o. R ) )
7		relexp1g	|- ( R e. V -> ( R ^r 1 ) = R )
8	7	coeq1d	|- ( R e. V -> ( ( R ^r 1 ) o. R ) = ( R o. R ) )
9	3 6 8	3eqtrd	|- ( R e. V -> ( R ^r 2 ) = ( R o. R ) )