Metamath Proof Explorer


Theorem ndmima

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 𝐵 → ( 𝐵 “ { 𝐴 } ) = ∅ )