difsnexi

Description: If the difference of a class and a singleton is a set, the class itself is a set. (Contributed by AV, 15-Jan-2019)

		Ref	Expression
	Assertion	difsnexi	$⊢ N ∖ \{K\} \in V \to N \in V$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (K \in N \land N ∖ \{K\} \in V) \to N ∖ \{K\} \in V$
2		snex	$⊢ \{K\} \in V$
3		unexg	$⊢ (N ∖ \{K\} \in V \land \{K\} \in V) \to (N ∖ \{K\}) \cup \{K\} \in V$
4	1 2 3	sylancl	$⊢ (K \in N \land N ∖ \{K\} \in V) \to (N ∖ \{K\}) \cup \{K\} \in V$
5		difsnid	$⊢ K \in N \to (N ∖ \{K\}) \cup \{K\} = N$
6	5	eqcomd	$⊢ K \in N \to N = (N ∖ \{K\}) \cup \{K\}$
7	6	eleq1d	$⊢ K \in N \to (N \in V \leftrightarrow (N ∖ \{K\}) \cup \{K\} \in V)$
8	7	adantr	$⊢ (K \in N \land N ∖ \{K\} \in V) \to (N \in V \leftrightarrow (N ∖ \{K\}) \cup \{K\} \in V)$
9	4 8	mpbird	$⊢ (K \in N \land N ∖ \{K\} \in V) \to N \in V$
10	9	ex	$⊢ K \in N \to (N ∖ \{K\} \in V \to N \in V)$
11		difsn	$⊢ \neg K \in N \to N ∖ \{K\} = N$
12	11	eleq1d	$⊢ \neg K \in N \to (N ∖ \{K\} \in V \leftrightarrow N \in V)$
13	12	biimpd	$⊢ \neg K \in N \to (N ∖ \{K\} \in V \to N \in V)$
14	10 13	pm2.61i	$⊢ N ∖ \{K\} \in V \to N \in V$

Metamath Proof Explorer