Theorem prid2 3690

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 3689	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 3659	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2245	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2141  Vcvv 2730  {cpr 3584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590

This theorem is referenced by:  prel12  3758  opi2  4218  opeluu  4435  ontr2exmid  4509  onsucelsucexmid  4514  regexmidlemm  4516  ordtri2or2exmid  4555  ontri2orexmidim  4556  dmrnssfld  4874  funopg  5232  acexmidlema  5844  acexmidlemcase  5848  acexmidlem2  5850  1lt2o  6421  2dom  6783  unfiexmid  6895  djuss  7047  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  cnelprrecn  7910  mnfxr  7976  sup3exmid  8873  m1expcl2  10498  lgsdir2lem3  13725  bdop  13910  2o01f  14029  iswomni0  14083