Theorem enp1ilem

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

	Ref	Expression
Hypothesis	enp1ilem.1	⊢ 𝑇 = ( { 𝑥 } ∪ 𝑆 )
Assertion	enp1ilem	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑥 } ) = 𝑆 → 𝐴 = 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		enp1ilem.1	⊢ 𝑇 = ( { 𝑥 } ∪ 𝑆 )
2		uneq1	⊢ ( ( 𝐴 ∖ { 𝑥 } ) = 𝑆 → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝑆 ∪ { 𝑥 } ) )
3		undif1	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝐴 ∪ { 𝑥 } )
4		uncom	⊢ ( 𝑆 ∪ { 𝑥 } ) = ( { 𝑥 } ∪ 𝑆 )
5	4 1	eqtr4i	⊢ ( 𝑆 ∪ { 𝑥 } ) = 𝑇
6	2 3 5	3eqtr3g	⊢ ( ( 𝐴 ∖ { 𝑥 } ) = 𝑆 → ( 𝐴 ∪ { 𝑥 } ) = 𝑇 )
7		snssi	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ 𝐴 )
8		ssequn2	⊢ ( { 𝑥 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 𝑥 } ) = 𝐴 )
9	7 8	sylib	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∪ { 𝑥 } ) = 𝐴 )
10	9	eqeq1d	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∪ { 𝑥 } ) = 𝑇 ↔ 𝐴 = 𝑇 ) )
11	6 10	imbitrid	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑥 } ) = 𝑆 → 𝐴 = 𝑇 ) )