Theorem prid2 4242

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 4241	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4211	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2686	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 1977  Vcvv 3173  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  prel12  4323  opi2  4865  opeluu  4866  opthwiener  4901  dmrnssfld  5305  funopg  5836  2dom  7915  dfac2  8836  brdom7disj  9234  brdom6disj  9235  cnelprrecn  9908  mnfxr  9975  m1expcl2  12744  hash2prb  13111  pr2pwpr  13116  sadcf  15013  xpsfrnel2  16048  setcepi  16561  grpss  17263  efgi1  17957  frgpuptinv  18007  dmdprdpr  18271  dprdpr  18272  cnmsgnsubg  19742  m2detleiblem6  20251  m2detleiblem3  20254  m2detleiblem4  20255  m2detleib  20256  indiscld  20705  xpstopnlem1  21422  xpstopnlem2  21424  i1f1lem  23262  i1f1  23263  aannenlem2  23888  taylthlem2  23932  ppiublem2  24728  lgsdir2lem3  24852  ecgrtg  25663  elntg  25664  wlkntrl  26092  usgra2wlkspthlem2  26148  constr3lem4  26175  usg2wlkonot  26410  usg2wotspth  26411  eupath  26508  ex-br  26680  ex-eprel  26682  subfacp1lem3  30418  kur14lem7  30448  fprb  30916  sltres  31061  noxp2o  31064  nobndup  31099  onpsstopbas  31599  onint1  31618  bj-inftyexpidisj  32274  kelac2  36653  fvrcllb1d  37006  relexp1idm  37025  corcltrcl  37050  cotrclrcl  37053  clsk1indlem1  37363  refsum2cnlem1  38219  fourierdlem103  39102  fourierdlem104  39103  ioorrnopn  39201  ioorrnopnxr  39203  usgr2trlncl  40966  umgrwwlks2on  41161  1wlk2v2e  41324  eulerpathpr  41408  zlmodzxzscm  41928  zlmodzxzldeplem3  42085  nn0sumshdiglemB  42212