Metamath Proof Explorer

Theorem dfatafv2ex

Description: The alternate function value at a class A is always a set if the function/class F is defined at A . (Contributed by AV, 6-Sep-2022)

Ref Expression
Assertion dfatafv2ex 
|- ( F defAt A -> ( F '''' A ) e. _V )

Proof

Step Hyp Ref Expression
1 dfatafv2iota 
 |-  ( F defAt A -> ( F '''' A ) = ( iota x A F x ) )
2 iotaex 
 |-  ( iota x A F x ) e. _V
3 1 2 eqeltrdi 
 |-  ( F defAt A -> ( F '''' A ) e. _V )