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 ⊢ B ∈ V
Assertion prid2 ⊢ B ∈ A B

Proof

Step Hyp Ref Expression
1 prid2.1 ⊢ B ∈ V
2 1 prid1 ⊢ B ∈ B A
3 prcom ⊢ B A = A B
4 2 3 eleqtri ⊢ B ∈ A B