Metamath Proof Explorer


Theorem brfvid

Description: If two elements are connected by a value of the identity relation, then they are connected via the argument. (Contributed by RP, 21-Jul-2020)

Ref Expression
Hypothesis brfvid.r φ R V
Assertion brfvid φ A I R B A R B

Proof

Step Hyp Ref Expression
1 brfvid.r φ R V
2 fvi R V I R = R
3 1 2 syl φ I R = R
4 3 breqd φ A I R B A R B