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	|- ( ph -> R e. V )
Assertion	relexp1d	|- ( ph -> ( R ^r 1 ) = R )

Proof

Step	Hyp	Ref	Expression
1		relexp1d.1	|- ( ph -> R e. V )
2		relexp1g	|- ( R e. V -> ( R ^r 1 ) = R )
3	1 2	syl	|- ( ph -> ( R ^r 1 ) = R )