Metamath Proof Explorer
Description: The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998) (Proof shortened by OpenAI, 3-Jul-2020)
|
|
Ref |
Expression |
|
Assertion |
ndmima |
⊢ ( ¬ 𝐴 ∈ dom 𝐵 → ( 𝐵 “ { 𝐴 } ) = ∅ ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
imadisj |
⊢ ( ( 𝐵 “ { 𝐴 } ) = ∅ ↔ ( dom 𝐵 ∩ { 𝐴 } ) = ∅ ) |
2 |
|
disjsn |
⊢ ( ( dom 𝐵 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ dom 𝐵 ) |
3 |
1 2
|
sylbbr |
⊢ ( ¬ 𝐴 ∈ dom 𝐵 → ( 𝐵 “ { 𝐴 } ) = ∅ ) |