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	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	brfvid	⊢ ( 𝜑 → ( 𝐴 ( I ‘ 𝑅 ) 𝐵 ↔ 𝐴 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brfvid.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		fvi	⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
3	1 2	syl	⊢ ( 𝜑 → ( I ‘ 𝑅 ) = 𝑅 )
4	3	breqd	⊢ ( 𝜑 → ( 𝐴 ( I ‘ 𝑅 ) 𝐵 ↔ 𝐴 𝑅 𝐵 ) )