# Metamath Proof Explorer

## Theorem ackbij1lem1

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion ackbij1lem1 ${⊢}¬{A}\in {B}\to {B}\cap \mathrm{suc}{A}={B}\cap {A}$

### Proof

Step Hyp Ref Expression
1 df-suc ${⊢}\mathrm{suc}{A}={A}\cup \left\{{A}\right\}$
2 1 ineq2i ${⊢}{B}\cap \mathrm{suc}{A}={B}\cap \left({A}\cup \left\{{A}\right\}\right)$
3 indi ${⊢}{B}\cap \left({A}\cup \left\{{A}\right\}\right)=\left({B}\cap {A}\right)\cup \left({B}\cap \left\{{A}\right\}\right)$
4 2 3 eqtri ${⊢}{B}\cap \mathrm{suc}{A}=\left({B}\cap {A}\right)\cup \left({B}\cap \left\{{A}\right\}\right)$
5 disjsn ${⊢}{B}\cap \left\{{A}\right\}=\varnothing ↔¬{A}\in {B}$
6 5 biimpri ${⊢}¬{A}\in {B}\to {B}\cap \left\{{A}\right\}=\varnothing$
7 6 uneq2d ${⊢}¬{A}\in {B}\to \left({B}\cap {A}\right)\cup \left({B}\cap \left\{{A}\right\}\right)=\left({B}\cap {A}\right)\cup \varnothing$
8 un0 ${⊢}\left({B}\cap {A}\right)\cup \varnothing ={B}\cap {A}$
9 7 8 syl6eq ${⊢}¬{A}\in {B}\to \left({B}\cap {A}\right)\cup \left({B}\cap \left\{{A}\right\}\right)={B}\cap {A}$
10 4 9 syl5eq ${⊢}¬{A}\in {B}\to {B}\cap \mathrm{suc}{A}={B}\cap {A}$