Theorem opid

Description: The ordered pair <. A , A >. in Kuratowski's representation. Inference form of opidg . (Contributed by FL, 28-Dec-2011) (Proof shortened by AV, 16-Feb-2022) (Avoid depending on this detail.)

	Ref	Expression
Hypothesis	opid.1	⊢ 𝐴 ∈ V
Assertion	opid	⊢ ⟨ 𝐴 , 𝐴 ⟩ = { { 𝐴 } }

Proof

Step	Hyp	Ref	Expression
1		opid.1	⊢ 𝐴 ∈ V
2		opidg	⊢ ( 𝐴 ∈ V → ⟨ 𝐴 , 𝐴 ⟩ = { { 𝐴 } } )
3	1 2	ax-mp	⊢ ⟨ 𝐴 , 𝐴 ⟩ = { { 𝐴 } }