This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )