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 } ) e. _V -> N e. _V )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( K e. N /\ ( N \ { K } ) e. _V ) -> ( N \ { K } ) e. _V )
2		snex	|- { K } e. _V
3		unexg	|- ( ( ( N \ { K } ) e. _V /\ { K } e. _V ) -> ( ( N \ { K } ) u. { K } ) e. _V )
4	1 2 3	sylancl	|- ( ( K e. N /\ ( N \ { K } ) e. _V ) -> ( ( N \ { K } ) u. { K } ) e. _V )
5		difsnid	|- ( K e. N -> ( ( N \ { K } ) u. { K } ) = N )
6	5	eqcomd	|- ( K e. N -> N = ( ( N \ { K } ) u. { K } ) )
7	6	eleq1d	|- ( K e. N -> ( N e. _V <-> ( ( N \ { K } ) u. { K } ) e. _V ) )
8	7	adantr	|- ( ( K e. N /\ ( N \ { K } ) e. _V ) -> ( N e. _V <-> ( ( N \ { K } ) u. { K } ) e. _V ) )
9	4 8	mpbird	|- ( ( K e. N /\ ( N \ { K } ) e. _V ) -> N e. _V )
10	9	ex	|- ( K e. N -> ( ( N \ { K } ) e. _V -> N e. _V ) )
11		difsn	|- ( -. K e. N -> ( N \ { K } ) = N )
12	11	eleq1d	|- ( -. K e. N -> ( ( N \ { K } ) e. _V <-> N e. _V ) )
13	12	biimpd	|- ( -. K e. N -> ( ( N \ { K } ) e. _V -> N e. _V ) )
14	10 13	pm2.61i	|- ( ( N \ { K } ) e. _V -> N e. _V )