en1eqsn

Description: A set with one element is a singleton. (Contributed by FL, 18-Aug-2008) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 4-Jan-2025)

		Ref	Expression
	Assertion	en1eqsn	$⊢ (A \in B \land B \approx 1_{𝑜}) \to B = \{A\}$

Step	Hyp	Ref	Expression
1		en1	$⊢ B \approx 1_{𝑜} \leftrightarrow \exists x B = \{x\}$
2		eleq2	$⊢ B = \{x\} \to (A \in B \leftrightarrow A \in \{x\})$
3		elsni	$⊢ A \in \{x\} \to A = x$
4	3	sneqd	$⊢ A \in \{x\} \to \{A\} = \{x\}$
5	2 4	biimtrdi	$⊢ B = \{x\} \to (A \in B \to \{A\} = \{x\})$
6	5	imp	$⊢ (B = \{x\} \land A \in B) \to \{A\} = \{x\}$
7		eqtr3	$⊢ (B = \{x\} \land \{A\} = \{x\}) \to B = \{A\}$
8	6 7	syldan	$⊢ (B = \{x\} \land A \in B) \to B = \{A\}$
9	8	ex	$⊢ B = \{x\} \to (A \in B \to B = \{A\})$
10	9	exlimiv	$⊢ \exists x B = \{x\} \to (A \in B \to B = \{A\})$
11	1 10	sylbi	$⊢ B \approx 1_{𝑜} \to (A \in B \to B = \{A\})$
12	11	impcom	$⊢ (A \in B \land B \approx 1_{𝑜}) \to B = \{A\}$

Metamath Proof Explorer