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

Metamath Proof Explorer

Theorem elpwdifsn

Description: A subset of a set is an element of the power set of the difference of the set with a singleton if the subset does not contain the singleton element. (Contributed by AV, 10-Jan-2020)

Ref Expression
Assertion elpwdifsn ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → 𝑆 ∈ 𝒫 ( 𝑉 ∖ { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → 𝑆 ⊆ 𝑉 )
2 1 sselda ⊢ ( ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑉 )
3 df-nel ⊢ ( 𝐴 ∉ 𝑆 ↔ ¬ 𝐴 ∈ 𝑆 )
4 3 biimpi ⊢ ( 𝐴 ∉ 𝑆 → ¬ 𝐴 ∈ 𝑆 )
5 4 3ad2ant3 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → ¬ 𝐴 ∈ 𝑆 )
6 5 anim1ci ⊢ ( ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆 ) )
7 nelne2 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆 ) → 𝑥 ≠ 𝐴 )
8 6 7 syl ⊢ ( ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ≠ 𝐴 )
9 eldifsn ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝐴 ) )
10 2 8 9 sylanbrc ⊢ ( ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) )
11 10 ex ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
12 11 ssrdv ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → 𝑆 ⊆ ( 𝑉 ∖ { 𝐴 } ) )
13 elpwg ⊢ ( 𝑆 ∈ 𝑊 → ( 𝑆 ∈ 𝒫 ( 𝑉 ∖ { 𝐴 } ) ↔ 𝑆 ⊆ ( 𝑉 ∖ { 𝐴 } ) ) )
14 13 3ad2ant1 ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → ( 𝑆 ∈ 𝒫 ( 𝑉 ∖ { 𝐴 } ) ↔ 𝑆 ⊆ ( 𝑉 ∖ { 𝐴 } ) ) )
15 12 14 mpbird ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → 𝑆 ∈ 𝒫 ( 𝑉 ∖ { 𝐴 } ) )