Theorem prid2 3725

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
prid2.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
prid2	⊢ 𝐵 ∈ {𝐴, 𝐵}

Proof of Theorem prid2

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

Syntax hints:   ∈ wcel 2164  Vcvv 2760  {cpr 3619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625

This theorem is referenced by:  prel12  3797  opi2  4262  opeluu  4481  ontr2exmid  4557  onsucelsucexmid  4562  regexmidlemm  4564  ordtri2or2exmid  4603  ontri2orexmidim  4604  dmrnssfld  4925  funopg  5288  acexmidlema  5909  acexmidlemcase  5913  acexmidlem2  5915  1lt2o  6495  2dom  6859  unfiexmid  6974  djuss  7129  exmidonfinlem  7253  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  cnelprrecn  8008  mnfxr  8076  sup3exmid  8976  m1expcl2  10632  fnpr2ob  12923  lgsdir2lem3  15146  bdop  15367  2o01f  15487  iswomni0  15541