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	⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ∧ 𝐴 ∉ 𝑆 ) → 𝑆 ∈ 𝒫 ( 𝑉 ∖ { 𝐴 } ) )