Theorem cnvsn

Description: Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998) (Revised by Mario Carneiro, 26-Apr-2015) (Proof shortened by BJ, 12-Feb-2022)

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

Proof

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