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	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		pwwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
2		snsspw	⊢ { 𝐴 } ⊆ 𝒫 𝐴
3		sswf	⊢ ( ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐴 } ⊆ 𝒫 𝐴 ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
4	2 3	mpan2	⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
5	1 4	sylbi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )