Theorem en1b

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015) Avoid ax-un . (Revised by BTernaryTau, 24-Sep-2024)

	Ref	Expression
Assertion	en1b	⊢ ( 𝐴 ≈ 1o ↔ 𝐴 = { ∪ 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		en1	⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
2		id	⊢ ( 𝐴 = { 𝑥 } → 𝐴 = { 𝑥 } )
3		unieq	⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = ∪ { 𝑥 } )
4		unisnv	⊢ ∪ { 𝑥 } = 𝑥
5	3 4	eqtrdi	⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = 𝑥 )
6	5	sneqd	⊢ ( 𝐴 = { 𝑥 } → { ∪ 𝐴 } = { 𝑥 } )
7	2 6	eqtr4d	⊢ ( 𝐴 = { 𝑥 } → 𝐴 = { ∪ 𝐴 } )
8	7	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐴 = { ∪ 𝐴 } )
9	1 8	sylbi	⊢ ( 𝐴 ≈ 1o → 𝐴 = { ∪ 𝐴 } )
10		id	⊢ ( 𝐴 = { ∪ 𝐴 } → 𝐴 = { ∪ 𝐴 } )
11		eqsnuniex	⊢ ( 𝐴 = { ∪ 𝐴 } → ∪ 𝐴 ∈ V )
12		ensn1g	⊢ ( ∪ 𝐴 ∈ V → { ∪ 𝐴 } ≈ 1o )
13	11 12	syl	⊢ ( 𝐴 = { ∪ 𝐴 } → { ∪ 𝐴 } ≈ 1o )
14	10 13	eqbrtrd	⊢ ( 𝐴 = { ∪ 𝐴 } → 𝐴 ≈ 1o )
15	9 14	impbii	⊢ ( 𝐴 ≈ 1o ↔ 𝐴 = { ∪ 𝐴 } )