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 i^i { A } ) = (/)

Proof

Step	Hyp	Ref	Expression
1		elirr	|- -. A e. A
2		elin	|- ( x e. ( A i^i { A } ) <-> ( x e. A /\ x e. { A } ) )
3		velsn	|- ( x e. { A } <-> x = A )
4		eleq1	|- ( x = A -> ( x e. A <-> A e. A ) )
5	4	biimpac	|- ( ( x e. A /\ x = A ) -> A e. A )
6	3 5	sylan2b	|- ( ( x e. A /\ x e. { A } ) -> A e. A )
7	2 6	sylbi	|- ( x e. ( A i^i { A } ) -> A e. A )
8	7	exlimiv	|- ( E. x x e. ( A i^i { A } ) -> A e. A )
9	1 8	mto	|- -. E. x x e. ( A i^i { A } )
10		n0	|- ( ( A i^i { A } ) =/= (/) <-> E. x x e. ( A i^i { A } ) )
11	9 10	mtbir	|- -. ( A i^i { A } ) =/= (/)
12		nne	|- ( -. ( A i^i { A } ) =/= (/) <-> ( A i^i { A } ) = (/) )
13	11 12	mpbi	|- ( A i^i { A } ) = (/)