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	$$⊢\phi \to R\in V$$
Assertion	relexp1d	$$⊢\phi \to R{\uparrow }_{r}1=R$$

Proof

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