Metamath Proof Explorer

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 ⊢ N ∖ K ∈ V → N ∈ V

Proof

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