Theorem brfvimex

Description: If a binary relation holds and the relation is the value of a function, then the argument to that function is a set. (Contributed by RP, 22-May-2021)

	Ref	Expression
Hypotheses	brfvimex.br	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
	brfvimex.fv	⊢ ( 𝜑 → 𝑅 = ( 𝐹 ‘ 𝐶 ) )
Assertion	brfvimex	⊢ ( 𝜑 → 𝐶 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		brfvimex.br	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
2		brfvimex.fv	⊢ ( 𝜑 → 𝑅 = ( 𝐹 ‘ 𝐶 ) )
3	2 1	breqdi	⊢ ( 𝜑 → 𝐴 ( 𝐹 ‘ 𝐶 ) 𝐵 )
4		brne0	⊢ ( 𝐴 ( 𝐹 ‘ 𝐶 ) 𝐵 → ( 𝐹 ‘ 𝐶 ) ≠ ∅ )
5		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( 𝐹 ‘ 𝐶 ) = ∅ )
6	5	necon1ai	⊢ ( ( 𝐹 ‘ 𝐶 ) ≠ ∅ → 𝐶 ∈ V )
7	3 4 6	3syl	⊢ ( 𝜑 → 𝐶 ∈ V )