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	|- A e. _V
Assertion	opid	|- <. A , A >. = { { A } }

Proof

Step	Hyp	Ref	Expression
1		opid.1	|- A e. _V
2		opidg	|- ( A e. _V -> <. A , A >. = { { A } } )
3	1 2	ax-mp	|- <. A , A >. = { { A } }