Theorem disjdifprg2

Description: A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016)

	Ref	Expression
Assertion	disjdifprg2	$$⊢A\in V\to \underset{x\in \left\{A\setminus B,A\cap B\right\}}{Disj}x$$

Proof

Step	Hyp	Ref	Expression
1		inex1g	$$⊢A\in V\to A\cap B\in \mathrm{V}$$
2		elex	$$⊢A\in V\to A\in \mathrm{V}$$
3		disjdifprg	$$⊢\left(A\cap B\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \underset{x\in \left\{A\setminus \left(A\cap B\right),A\cap B\right\}}{Disj}x$$
4	1 2 3	syl2anc	$$⊢A\in V\to \underset{x\in \left\{A\setminus \left(A\cap B\right),A\cap B\right\}}{Disj}x$$
5		difin	$$⊢A\setminus \left(A\cap B\right)=A\setminus B$$
6	5	preq1i	$$⊢\left\{A\setminus \left(A\cap B\right),A\cap B\right\}=\left\{A\setminus B,A\cap B\right\}$$
7	6	a1i	$$⊢A\in V\to \left\{A\setminus \left(A\cap B\right),A\cap B\right\}=\left\{A\setminus B,A\cap B\right\}$$
8	7	disjeq1d	$$⊢A\in V\to \left(\underset{x\in \left\{A\setminus \left(A\cap B\right),A\cap B\right\}}{Disj}x\leftrightarrow \underset{x\in \left\{A\setminus B,A\cap B\right\}}{Disj}x\right)$$
9	4 8	mpbid	$$⊢A\in V\to \underset{x\in \left\{A\setminus B,A\cap B\right\}}{Disj}x$$