This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prid2

Description: An unordered pair contains its second member. Part of Theorem 7.6 of Quine p. 49. (Note: the proof from prid2g and ax-mp has one fewer essential step but one more total step.) (Contributed by NM, 5-Aug-1993)

		Ref	Expression
	Hypothesis	prid2.1	⊢ 𝐵 ∈ V
	Assertion	prid2	⊢ 𝐵 ∈ { 𝐴 , 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		prid2.1	⊢ 𝐵 ∈ V
2	1	prid1	⊢ 𝐵 ∈ { 𝐵 , 𝐴 }
3		prcom	⊢ { 𝐵 , 𝐴 } = { 𝐴 , 𝐵 }
4	2 3	eleqtri	⊢ 𝐵 ∈ { 𝐴 , 𝐵 }