Theorem relexp1d

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

	Ref	Expression
Hypothesis	relexp1d.2	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	relexp1d	$$⊢\phi \to R{\uparrow }_{r}1=R$$

Proof

Step	Hyp	Ref	Expression
1		relexp1d.2	$$⊢\phi \to R\in \mathrm{V}$$
2		relexp1g	$$⊢R\in \mathrm{V}\to R{\uparrow }_{r}1=R$$
3	1 2	syl	$$⊢\phi \to R{\uparrow }_{r}1=R$$