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	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	brfvid	$$⊢\phi \to \left(A\mathrm{I}\left(R\right)B\leftrightarrow ARB\right)$$

Proof

Step	Hyp	Ref	Expression
1		brfvid.r	$$⊢\phi \to R\in \mathrm{V}$$
2		fvi	$$⊢R\in \mathrm{V}\to \mathrm{I}\left(R\right)=R$$
3	1 2	syl	$$⊢\phi \to \mathrm{I}\left(R\right)=R$$
4	3	breqd	$$⊢\phi \to \left(A\mathrm{I}\left(R\right)B\leftrightarrow ARB\right)$$