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	$⊢ (S \in W \land S \subseteq V \land A \notin S) \to S \in 𝒫 (V ∖ \{A\})$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (S \in W \land S \subseteq V \land A \notin S) \to S \subseteq V$
2	1	sselda	$⊢ ((S \in W \land S \subseteq V \land A \notin S) \land x \in S) \to x \in V$
3		df-nel	$⊢ A \notin S \leftrightarrow \neg A \in S$
4	3	biimpi	$⊢ A \notin S \to \neg A \in S$
5	4	3ad2ant3	$⊢ (S \in W \land S \subseteq V \land A \notin S) \to \neg A \in S$
6	5	anim1ci	$⊢ ((S \in W \land S \subseteq V \land A \notin S) \land x \in S) \to (x \in S \land \neg A \in S)$
7		nelne2	$⊢ (x \in S \land \neg A \in S) \to x \neq A$
8	6 7	syl	$⊢ ((S \in W \land S \subseteq V \land A \notin S) \land x \in S) \to x \neq A$
9	2 8	eldifsnd	$⊢ ((S \in W \land S \subseteq V \land A \notin S) \land x \in S) \to x \in (V ∖ \{A\})$
10	9	ex	$⊢ (S \in W \land S \subseteq V \land A \notin S) \to (x \in S \to x \in (V ∖ \{A\}))$
11	10	ssrdv	$⊢ (S \in W \land S \subseteq V \land A \notin S) \to S \subseteq V ∖ \{A\}$
12		elpwg	$⊢ S \in W \to (S \in 𝒫 (V ∖ \{A\}) \leftrightarrow S \subseteq V ∖ \{A\})$
13	12	3ad2ant1	$⊢ (S \in W \land S \subseteq V \land A \notin S) \to (S \in 𝒫 (V ∖ \{A\}) \leftrightarrow S \subseteq V ∖ \{A\})$
14	11 13	mpbird	$⊢ (S \in W \land S \subseteq V \land A \notin S) \to S \in 𝒫 (V ∖ \{A\})$