Theorem imadisjlnd

Description: Deduction form of one negated side of imadisj . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypothesis	imadisjlnd.1	⊢ ( 𝜑 → ( dom 𝐴 ∩ 𝐵 ) ≠ ∅ )
Assertion	imadisjlnd	⊢ ( 𝜑 → ( 𝐴 “ 𝐵 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		imadisjlnd.1	⊢ ( 𝜑 → ( dom 𝐴 ∩ 𝐵 ) ≠ ∅ )
2		imadisj	⊢ ( ( 𝐴 “ 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ 𝐵 ) = ∅ )
3	2	biimpi	⊢ ( ( 𝐴 “ 𝐵 ) = ∅ → ( dom 𝐴 ∩ 𝐵 ) = ∅ )
4	3	necon3i	⊢ ( ( dom 𝐴 ∩ 𝐵 ) ≠ ∅ → ( 𝐴 “ 𝐵 ) ≠ ∅ )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐴 “ 𝐵 ) ≠ ∅ )