Metamath Proof Explorer

Theorem fvex

Description: The value of a class exists. Corollary 6.13 of TakeutiZaring p. 27. (Contributed by NM, 30-Dec-1996)

Ref Expression
Assertion fvex F A V


Step Hyp Ref Expression
1 df-fv F A = ι x | A F x
2 iotaex ι x | A F x V
3 1 2 eqeltri F A V