Metamath Proof Explorer
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 |
⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∈ V ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
dfatafv2iota |
⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = ( ℩ 𝑥 𝐴 𝐹 𝑥 ) ) |
2 |
|
iotaex |
⊢ ( ℩ 𝑥 𝐴 𝐹 𝑥 ) ∈ V |
3 |
1 2
|
eqeltrdi |
⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∈ V ) |