Theorem enp1ilem

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

	Ref	Expression
Hypothesis	enp1ilem.1	$$⊢T=\left\{x\right\}\cup S$$
Assertion	enp1ilem	$$⊢x\in A\to \left(A\setminus \left\{x\right\}=S\to A=T\right)$$

Proof

Step	Hyp	Ref	Expression
1		enp1ilem.1	$$⊢T=\left\{x\right\}\cup S$$
2		uneq1	$$⊢A\setminus \left\{x\right\}=S\to \left(A\setminus \left\{x\right\}\right)\cup \left\{x\right\}=S\cup \left\{x\right\}$$
3		undif1	$$⊢\left(A\setminus \left\{x\right\}\right)\cup \left\{x\right\}=A\cup \left\{x\right\}$$
4		uncom	$$⊢S\cup \left\{x\right\}=\left\{x\right\}\cup S$$
5	4 1	eqtr4i	$$⊢S\cup \left\{x\right\}=T$$
6	2 3 5	3eqtr3g	$$⊢A\setminus \left\{x\right\}=S\to A\cup \left\{x\right\}=T$$
7		snssi	$$⊢x\in A\to \left\{x\right\}\subseteq A$$
8		ssequn2	$$⊢\left\{x\right\}\subseteq A\leftrightarrow A\cup \left\{x\right\}=A$$
9	7 8	sylib	$$⊢x\in A\to A\cup \left\{x\right\}=A$$
10	9	eqeq1d	$$⊢x\in A\to \left(A\cup \left\{x\right\}=T\leftrightarrow A=T\right)$$
11	6 10	syl5ib	$$⊢x\in A\to \left(A\setminus \left\{x\right\}=S\to A=T\right)$$