This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ A \approx 1_{𝑜} \leftrightarrow A = \{⋃ A\}$

Proof

Step	Hyp	Ref	Expression
1		en1	$⊢ A \approx 1_{𝑜} \leftrightarrow \exists x A = \{x\}$
2		id	$⊢ A = \{x\} \to A = \{x\}$
3		unieq	$⊢ A = \{x\} \to ⋃ A = ⋃ \{x\}$
4		unisnv	$⊢ ⋃ \{x\} = x$
5	3 4	eqtrdi	$⊢ A = \{x\} \to ⋃ A = x$
6	5	sneqd	$⊢ A = \{x\} \to \{⋃ A\} = \{x\}$
7	2 6	eqtr4d	$⊢ A = \{x\} \to A = \{⋃ A\}$
8	7	exlimiv	$⊢ \exists x A = \{x\} \to A = \{⋃ A\}$
9	1 8	sylbi	$⊢ A \approx 1_{𝑜} \to A = \{⋃ A\}$
10		id	$⊢ A = \{⋃ A\} \to A = \{⋃ A\}$
11		eqsnuniex	$⊢ A = \{⋃ A\} \to ⋃ A \in V$
12		ensn1g	$⊢ ⋃ A \in V \to \{⋃ A\} \approx 1_{𝑜}$
13	11 12	syl	$⊢ A = \{⋃ A\} \to \{⋃ A\} \approx 1_{𝑜}$
14	10 13	eqbrtrd	$⊢ A = \{⋃ A\} \to A \approx 1_{𝑜}$
15	9 14	impbii	$⊢ A \approx 1_{𝑜} \leftrightarrow A = \{⋃ A\}$