Metamath Proof Explorer


Theorem fvexd

Description: The value of a class exists (as consequent of anything). (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion fvexd φFAV

Proof

Step Hyp Ref Expression
1 fvex FAV
2 1 a1i φFAV