Metamath Proof Explorer


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 φ R V
Assertion relexp1d φ R r 1 = R

Proof

Step Hyp Ref Expression
1 relexp1d.1 φ R V
2 relexp1g R V R r 1 = R
3 1 2 syl φ R r 1 = R