Theorem nsnlpligALT

Description: Alternate version of nsnlplig using the predicate e/ instead of -. e. and whose proof is shorter. (Contributed by AV, 5-Dec-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nsnlpligALT	|- ( G e. Plig -> { A } e/ G )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U. G = U. G
2	1	l2p	|- ( ( G e. Plig /\ { A } e. G ) -> E. a e. U. G E. b e. U. G ( a =/= b /\ a e. { A } /\ b e. { A } ) )
3		elsni	|- ( a e. { A } -> a = A )
4		elsni	|- ( b e. { A } -> b = A )
5		eqtr3	|- ( ( a = A /\ b = A ) -> a = b )
6		eqneqall	|- ( a = b -> ( a =/= b -> { A } e/ G ) )
7	5 6	syl	|- ( ( a = A /\ b = A ) -> ( a =/= b -> { A } e/ G ) )
8	3 4 7	syl2an	|- ( ( a e. { A } /\ b e. { A } ) -> ( a =/= b -> { A } e/ G ) )
9	8	impcom	|- ( ( a =/= b /\ ( a e. { A } /\ b e. { A } ) ) -> { A } e/ G )
10	9	3impb	|- ( ( a =/= b /\ a e. { A } /\ b e. { A } ) -> { A } e/ G )
11	10	a1i	|- ( ( a e. U. G /\ b e. U. G ) -> ( ( a =/= b /\ a e. { A } /\ b e. { A } ) -> { A } e/ G ) )
12	11	rexlimivv	|- ( E. a e. U. G E. b e. U. G ( a =/= b /\ a e. { A } /\ b e. { A } ) -> { A } e/ G )
13	2 12	syl	|- ( ( G e. Plig /\ { A } e. G ) -> { A } e/ G )
14		simpr	|- ( ( G e. Plig /\ { A } e/ G ) -> { A } e/ G )
15	13 14	pm2.61danel	|- ( G e. Plig -> { A } e/ G )