This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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