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 ⊢ 𝑇 = ( { 𝑥 } ∪ 𝑆 )
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 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑥 } ) = 𝑆 → 𝐴 = 𝑇 ) )