Theorem bnj521

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj521	$$⊢A\cap \left\{A\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		elirr	$$⊢\neg A\in A$$
2		elin	$$⊢x\in \left(A\cap \left\{A\right\}\right)\leftrightarrow \left(x\in A\wedge x\in \left\{A\right\}\right)$$
3		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
4		eleq1	$$⊢x=A\to \left(x\in A\leftrightarrow A\in A\right)$$
5	4	biimpac	$$⊢\left(x\in A\wedge x=A\right)\to A\in A$$
6	3 5	sylan2b	$$⊢\left(x\in A\wedge x\in \left\{A\right\}\right)\to A\in A$$
7	2 6	sylbi	$$⊢x\in \left(A\cap \left\{A\right\}\right)\to A\in A$$
8	7	exlimiv	$$⊢\exists xx\in \left(A\cap \left\{A\right\}\right)\to A\in A$$
9	1 8	mto	$$⊢\neg \exists xx\in \left(A\cap \left\{A\right\}\right)$$
10		n0	$$⊢A\cap \left\{A\right\}\ne \varnothing \leftrightarrow \exists xx\in \left(A\cap \left\{A\right\}\right)$$
11	9 10	mtbir	$$⊢\neg A\cap \left\{A\right\}\ne \varnothing$$
12		nne	$$⊢\neg A\cap \left\{A\right\}\ne \varnothing \leftrightarrow A\cap \left\{A\right\}=\varnothing$$
13	11 12	mpbi	$$⊢A\cap \left\{A\right\}=\varnothing$$