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

Metamath Proof Explorer

Theorem enpr1g

Description: { A , A } has only one element. (Contributed by FL, 15-Feb-2010)

		Ref	Expression
	Assertion	enpr1g	$⊢ A \in V \to \{A, A\} \approx 1_{𝑜}$

Step	Hyp	Ref	Expression
1		dfsn2	$⊢ \{A\} = \{A, A\}$
2		ensn1g	$⊢ A \in V \to \{A\} \approx 1_{𝑜}$
3	1 2	eqbrtrrid	$⊢ A \in V \to \{A, A\} \approx 1_{𝑜}$