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 \{A ∖ B, A \cap B\}}{Disj} x$

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

Metamath Proof Explorer