Theorem prid2 4699

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4697 and ax-mp 5 has one fewer essential step but one more total step.) (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 4698	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4668	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2911	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2114  Vcvv 3494  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-pr 4570

This theorem is referenced by:  opi2  5361  opeluu  5362  opthwiener  5404  dmrnssfld  5841  funopg  6389  fprb  6956  2dom  8582  djuss  9349  dfac2b  9556  brdom7disj  9953  brdom6disj  9954  cnelprrecn  10630  mnfxr  10698  seqexw  13386  m1expcl2  13452  hash2prb  13831  pr2pwpr  13838  sadcf  15802  fnpr2ob  16831  setcepi  17348  grpss  18121  efgi1  18847  frgpuptinv  18897  dmdprdpr  19171  dprdpr  19172  cnmsgnsubg  20721  m2detleiblem6  21235  m2detleiblem3  21238  m2detleiblem4  21239  m2detleib  21240  indiscld  21699  xpstopnlem1  22417  xpstopnlem2  22419  ehl2eudis  24025  i1f1lem  24290  i1f1  24291  aannenlem2  24918  taylthlem2  24962  ppiublem2  25779  lgsdir2lem3  25903  ecgrtg  26769  elntg  26770  usgr2trlncl  27541  umgrwwlks2on  27736  wlk2v2e  27936  eulerpathpr  28019  ex-br  28210  ex-eprel  28212  s2rn  30620  trsp2cyc  30765  cyc3fv2  30780  subfacp1lem3  32429  kur14lem7  32459  ex-sategoelel12  32674  sltres  33169  noextendgt  33177  nolesgn2ores  33179  nosepnelem  33184  nosepdmlem  33187  nolt02o  33199  nosupno  33203  nosupbnd1lem3  33210  nosupbnd1  33214  nosupbnd2lem1  33215  onpsstopbas  33778  onint1  33797  bj-inftyexpidisj  34495  kelac2  39685  fvrcllb1d  40060  relexp1idm  40079  corcltrcl  40104  cotrclrcl  40107  clsk1indlem1  40415  mnuprdlem2  40629  mnuprdlem3  40630  mnurndlem1  40637  refsum2cnlem1  41314  limsup10exlem  42073  fourierdlem103  42514  fourierdlem104  42515  ioorrnopn  42610  ioorrnopnxr  42612  zlmodzxzscm  44425  zlmodzxzldeplem3  44577  nn0sumshdiglemB  44700  rrx2pyel  44719  rrx2linesl  44750  2sphere0  44757