ackbij1lem2

		Ref	Expression
	Assertion	ackbij1lem2	$⊢ A \in B \to B \cap suc A = \{A\} \cup (B \cap A)$

Step	Hyp	Ref	Expression
1		df-suc	$⊢ suc A = A \cup \{A\}$
2	1	ineq2i	$⊢ B \cap suc A = B \cap (A \cup \{A\})$
3		indi	$⊢ B \cap (A \cup \{A\}) = (B \cap A) \cup (B \cap \{A\})$
4		uncom	$⊢ (B \cap A) \cup (B \cap \{A\}) = (B \cap \{A\}) \cup (B \cap A)$
5	2 3 4	3eqtri	$⊢ B \cap suc A = (B \cap \{A\}) \cup (B \cap A)$
6		snssi	$⊢ A \in B \to \{A\} \subseteq B$
7		sseqin2	$⊢ \{A\} \subseteq B \leftrightarrow B \cap \{A\} = \{A\}$
8	6 7	sylib	$⊢ A \in B \to B \cap \{A\} = \{A\}$
9	8	uneq1d	$⊢ A \in B \to (B \cap \{A\}) \cup (B \cap A) = \{A\} \cup (B \cap A)$
10	5 9	eqtrid	$⊢ A \in B \to B \cap suc A = \{A\} \cup (B \cap A)$

Metamath Proof Explorer