Metamath Proof Explorer


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 )