Theorem enp1ilem

Description: Lemma for uses of enp1i . (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Hypothesis	enp1ilem.1	|- T = ( { x } u. S )
Assertion	enp1ilem	|- ( x e. A -> ( ( A \ { x } ) = S -> A = T ) )

Proof

Step	Hyp	Ref	Expression
1		enp1ilem.1	|- T = ( { x } u. S )
2		uneq1	|- ( ( A \ { x } ) = S -> ( ( A \ { x } ) u. { x } ) = ( S u. { x } ) )
3		undif1	|- ( ( A \ { x } ) u. { x } ) = ( A u. { x } )
4		uncom	|- ( S u. { x } ) = ( { x } u. S )
5	4 1	eqtr4i	|- ( S u. { x } ) = T
6	2 3 5	3eqtr3g	|- ( ( A \ { x } ) = S -> ( A u. { x } ) = T )
7		snssi	|- ( x e. A -> { x } C_ A )
8		ssequn2	|- ( { x } C_ A <-> ( A u. { x } ) = A )
9	7 8	sylib	|- ( x e. A -> ( A u. { x } ) = A )
10	9	eqeq1d	|- ( x e. A -> ( ( A u. { x } ) = T <-> A = T ) )
11	6 10	imbitrid	|- ( x e. A -> ( ( A \ { x } ) = S -> A = T ) )