Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Exploring Topology via Seifert and Threlfall
Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods
brfvimex
Metamath Proof Explorer
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 )