Theorem sdomdif

Description: The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013)

	Ref	Expression
Assertion	sdomdif	⊢ ( 𝐴 ≺ 𝐵 → ( 𝐵 ∖ 𝐴 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		relsdom	⊢ Rel ≺
2	1	brrelex1i	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ∈ V )
3		ssdif0	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∖ 𝐴 ) = ∅ )
4		ssdomg	⊢ ( 𝐴 ∈ V → ( 𝐵 ⊆ 𝐴 → 𝐵 ≼ 𝐴 ) )
5		domnsym	⊢ ( 𝐵 ≼ 𝐴 → ¬ 𝐴 ≺ 𝐵 )
6	4 5	syl6	⊢ ( 𝐴 ∈ V → ( 𝐵 ⊆ 𝐴 → ¬ 𝐴 ≺ 𝐵 ) )
7	3 6	biimtrrid	⊢ ( 𝐴 ∈ V → ( ( 𝐵 ∖ 𝐴 ) = ∅ → ¬ 𝐴 ≺ 𝐵 ) )
8	2 7	syl	⊢ ( 𝐴 ≺ 𝐵 → ( ( 𝐵 ∖ 𝐴 ) = ∅ → ¬ 𝐴 ≺ 𝐵 ) )
9	8	con2d	⊢ ( 𝐴 ≺ 𝐵 → ( 𝐴 ≺ 𝐵 → ¬ ( 𝐵 ∖ 𝐴 ) = ∅ ) )
10	9	pm2.43i	⊢ ( 𝐴 ≺ 𝐵 → ¬ ( 𝐵 ∖ 𝐴 ) = ∅ )
11	10	neqned	⊢ ( 𝐴 ≺ 𝐵 → ( 𝐵 ∖ 𝐴 ) ≠ ∅ )