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	$$⊢A\prec B\to B\setminus A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		relsdom	$$⊢\mathrm{Rel}\prec$$
2	1	brrelex1i	$$⊢A\prec B\to A\in \mathrm{V}$$
3		ssdif0	$$⊢B\subseteq A\leftrightarrow B\setminus A=\varnothing$$
4		ssdomg	$$⊢A\in \mathrm{V}\to \left(B\subseteq A\to B\preccurlyeq A\right)$$
5		domnsym	$$⊢B\preccurlyeq A\to \neg A\prec B$$
6	4 5	syl6	$$⊢A\in \mathrm{V}\to \left(B\subseteq A\to \neg A\prec B\right)$$
7	3 6	syl5bir	$$⊢A\in \mathrm{V}\to \left(B\setminus A=\varnothing \to \neg A\prec B\right)$$
8	2 7	syl	$$⊢A\prec B\to \left(B\setminus A=\varnothing \to \neg A\prec B\right)$$
9	8	con2d	$$⊢A\prec B\to \left(A\prec B\to \neg B\setminus A=\varnothing \right)$$
10	9	pm2.43i	$$⊢A\prec B\to \neg B\setminus A=\varnothing$$
11	10	neqned	$$⊢A\prec B\to B\setminus A\ne \varnothing$$