Theorem prid2 4298

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 4297	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4267	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2699	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 1990  Vcvv 3200  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  prel12  4383  opi2  4938  opeluu  4939  opthwiener  4976  dmrnssfld  5384  funopg  5922  2dom  8029  dfac2  8953  brdom7disj  9353  brdom6disj  9354  cnelprrecn  10029  mnfxr  10096  m1expcl2  12882  hash2prb  13254  pr2pwpr  13261  sadcf  15175  xpsfrnel2  16225  setcepi  16738  grpss  17440  efgi1  18134  frgpuptinv  18184  dmdprdpr  18448  dprdpr  18449  cnmsgnsubg  19923  m2detleiblem6  20432  m2detleiblem3  20435  m2detleiblem4  20436  m2detleib  20437  indiscld  20895  xpstopnlem1  21612  xpstopnlem2  21614  i1f1lem  23456  i1f1  23457  aannenlem2  24084  taylthlem2  24128  ppiublem2  24928  lgsdir2lem3  25052  ecgrtg  25863  elntg  25864  usgr2trlncl  26656  umgrwwlks2on  26850  wlk2v2e  27017  eulerpathpr  27100  ex-br  27288  ex-eprel  27290  subfacp1lem3  31164  kur14lem7  31194  fprb  31669  sltres  31815  noextendgt  31823  nolesgn2ores  31825  nosepnelem  31830  nosepdmlem  31833  nolt02o  31845  nosupno  31849  nosupbnd1lem3  31856  nosupbnd1  31860  nosupbnd2lem1  31861  onpsstopbas  32429  onint1  32448  bj-inftyexpidisj  33097  kelac2  37635  fvrcllb1d  37987  relexp1idm  38006  corcltrcl  38031  cotrclrcl  38034  clsk1indlem1  38343  refsum2cnlem1  39196  limsup10exlem  40004  fourierdlem103  40426  fourierdlem104  40427  ioorrnopn  40525  ioorrnopnxr  40527  zlmodzxzscm  42135  zlmodzxzldeplem3  42291  nn0sumshdiglemB  42414