ackbij1lem1

		Ref	Expression
	Assertion	ackbij1lem1	$⊢ \neg A \in B \to B \cap suc A = 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	2 3	eqtri	$⊢ B \cap suc A = (B \cap A) \cup (B \cap \{A\})$
5		disjsn	$⊢ B \cap \{A\} = \emptyset \leftrightarrow \neg A \in B$
6	5	biimpri	$⊢ \neg A \in B \to B \cap \{A\} = \emptyset$
7	6	uneq2d	$⊢ \neg A \in B \to (B \cap A) \cup (B \cap \{A\}) = (B \cap A) \cup \emptyset$
8		un0	$⊢ (B \cap A) \cup \emptyset = B \cap A$
9	7 8	eqtrdi	$⊢ \neg A \in B \to (B \cap A) \cup (B \cap \{A\}) = B \cap A$
10	4 9	eqtrid	$⊢ \neg A \in B \to B \cap suc A = B \cap A$

Metamath Proof Explorer