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	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	relexpcnvd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	relexpcnvd	⊢ ( 𝜑 → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		relexpcnvd.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
2		relexpcnvd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3		relexpcnv	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )
4	2 1 3	syl2anc	⊢ ( 𝜑 → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )