Theorem relexp1d

Description: A relation composed once is itself. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypothesis	relexp1d.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
Assertion	relexp1d	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		relexp1d.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
2		relexp1g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
3	1 2	syl	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )