Metamath Proof Explorer


Theorem fvexi

Description: The value of a class exists. Inference form of fvex . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis fvexi.1 ⊢ 𝐴 = ( 𝐹 ‘ 𝐵 )
Assertion fvexi 𝐴 ∈ V

Proof

Step Hyp Ref Expression
1 fvexi.1 ⊢ 𝐴 = ( 𝐹 ‘ 𝐵 )
2 fvex ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
3 1 2 eqeltri ⊢ 𝐴 ∈ V