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 ⊢ φ → A R B
brfvimex.fv ⊢ φ → R = F ⁡ C
Assertion brfvimex ⊢ φ → C ∈ V

Proof

Step Hyp Ref Expression
1 brfvimex.br ⊢ φ → A R B
2 brfvimex.fv ⊢ φ → R = F ⁡ C
3 2 1 breqdi ⊢ φ → A F ⁡ C B
4 brne0 ⊢ A F ⁡ C B → F ⁡ C ≠ ∅
5 fvprc ⊢ ¬ C ∈ V → F ⁡ C = ∅
6 5 necon1ai ⊢ F ⁡ C ≠ ∅ → C ∈ V
7 3 4 6 3syl ⊢ φ → C ∈ V