Metamath Proof Explorer


Theorem enp1ilem

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

Ref Expression
Hypothesis enp1ilem.1 T=xS
Assertion enp1ilem xAAx=SA=T

Proof

Step Hyp Ref Expression
1 enp1ilem.1 T=xS
2 uneq1 Ax=SAxx=Sx
3 undif1 Axx=Ax
4 uncom Sx=xS
5 4 1 eqtr4i Sx=T
6 2 3 5 3eqtr3g Ax=SAx=T
7 snssi xAxA
8 ssequn2 xAAx=A
9 7 8 sylib xAAx=A
10 9 eqeq1d xAAx=TA=T
11 6 10 imbitrid xAAx=SA=T