Description: A function's value at a proper class is the empty set. (Contributed by NM, 20-May-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | fvprc | ⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brprcneu | ⊢ ( ¬ 𝐴 ∈ V → ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ) | |
2 | tz6.12-2 | ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ‘ 𝐴 ) = ∅ ) | |
3 | 1 2 | syl | ⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ ) |