Metamath Proof Explorer


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 ) )