Theorem dfop

Description: Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	dfop.1	⊢ 𝐴 ∈ V
	dfop.2	⊢ 𝐵 ∈ V
Assertion	dfop	⊢ ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } }

Proof

Step	Hyp	Ref	Expression
1		dfop.1	⊢ 𝐴 ∈ V
2		dfop.2	⊢ 𝐵 ∈ V
3		dfopg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
4	1 2 3	mp2an	⊢ ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } }