Theorem 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	⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∈ V → 𝑁 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑁 ∖ { 𝐾 } ) ∈ V ) → ( 𝑁 ∖ { 𝐾 } ) ∈ V )
2		snex	⊢ { 𝐾 } ∈ V
3		unexg	⊢ ( ( ( 𝑁 ∖ { 𝐾 } ) ∈ V ∧ { 𝐾 } ∈ V ) → ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∈ V )
4	1 2 3	sylancl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑁 ∖ { 𝐾 } ) ∈ V ) → ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∈ V )
5		difsnid	⊢ ( 𝐾 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑁 )
6	5	eqcomd	⊢ ( 𝐾 ∈ 𝑁 → 𝑁 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
7	6	eleq1d	⊢ ( 𝐾 ∈ 𝑁 → ( 𝑁 ∈ V ↔ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∈ V ) )
8	7	adantr	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑁 ∖ { 𝐾 } ) ∈ V ) → ( 𝑁 ∈ V ↔ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∈ V ) )
9	4 8	mpbird	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑁 ∖ { 𝐾 } ) ∈ V ) → 𝑁 ∈ V )
10	9	ex	⊢ ( 𝐾 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∈ V → 𝑁 ∈ V ) )
11		difsn	⊢ ( ¬ 𝐾 ∈ 𝑁 → ( 𝑁 ∖ { 𝐾 } ) = 𝑁 )
12	11	eleq1d	⊢ ( ¬ 𝐾 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∈ V ↔ 𝑁 ∈ V ) )
13	12	biimpd	⊢ ( ¬ 𝐾 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∈ V → 𝑁 ∈ V ) )
14	10 13	pm2.61i	⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∈ V → 𝑁 ∈ V )