Theorem snwf

Description: A singleton is well-founded if its element is. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	snwf	|- ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )

Proof

Step	Hyp	Ref	Expression
1		pwwf	|- ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) )
2		snsspw	|- { A } C_ ~P A
3		sswf	|- ( ( ~P A e. U. ( R1 " On ) /\ { A } C_ ~P A ) -> { A } e. U. ( R1 " On ) )
4	2 3	mpan2	|- ( ~P A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
5	1 4	sylbi	|- ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )