Theorem enpr1g

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

	Ref	Expression
Assertion	enpr1g	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 , 𝐴 } ≈ 1o )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
2		ensn1g	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≈ 1o )
3	1 2	eqbrtrrid	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 , 𝐴 } ≈ 1o )