Theorem relexpcnvd

Description: Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	relexpcnvd.1	|- ( ph -> R e. V )
	relexpcnvd.2	|- ( ph -> N e. NN0 )
Assertion	relexpcnvd	|- ( ph -> `' ( R ^r N ) = ( `' R ^r N ) )

Proof

Step	Hyp	Ref	Expression
1		relexpcnvd.1	|- ( ph -> R e. V )
2		relexpcnvd.2	|- ( ph -> N e. NN0 )
3		relexpcnv	|- ( ( N e. NN0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
4	2 1 3	syl2anc	|- ( ph -> `' ( R ^r N ) = ( `' R ^r N ) )