Theorem indislem

Description: A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	indislem	|- { (/) , ( _I ` A ) } = { (/) , A }

Proof

Step	Hyp	Ref	Expression
1		fvi	|- ( A e. _V -> ( _I ` A ) = A )
2	1	preq2d	|- ( A e. _V -> { (/) , ( _I ` A ) } = { (/) , A } )
3		dfsn2	|- { (/) } = { (/) , (/) }
4	3	eqcomi	|- { (/) , (/) } = { (/) }
5		fvprc	|- ( -. A e. _V -> ( _I ` A ) = (/) )
6	5	preq2d	|- ( -. A e. _V -> { (/) , ( _I ` A ) } = { (/) , (/) } )
7		prprc2	|- ( -. A e. _V -> { (/) , A } = { (/) } )
8	4 6 7	3eqtr4a	|- ( -. A e. _V -> { (/) , ( _I ` A ) } = { (/) , A } )
9	2 8	pm2.61i	|- { (/) , ( _I ` A ) } = { (/) , A }