Theorem prid2 4696

Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4694 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 4695	. 2 ⊢ 𝐵 ∈ {𝐵, 𝐴}
3		prcom 4665	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
4	2, 3	eleqtri 2837	1 ⊢ 𝐵 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2119  Vcvv 3431  {cpr 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4557  df-pr 4559

This theorem is referenced by:  opi2  5410  opeluu  5411  opthwiener  5456  dmrnssfld  5917  funopg  6520  fprb  7139  nlim2  8416  2dom  8968  djuss  9836  dfac2b  10045  brdom7disj  10445  brdom6disj  10446  cnelprrecn  11123  mnfxr  11194  seqexw  13971  m1expcl2  14039  hash2prb  14426  pr2pwpr  14433  sadcf  16414  fnpr2ob  17514  setcepi  18047  setc2obas  18053  setc2ohom  18054  cat1  18056  grpss  18922  efgi1  19688  frgpuptinv  19738  dmdprdpr  20018  dprdpr  20019  cnmsgnsubg  21553  m2detleiblem6  22610  m2detleiblem3  22613  m2detleiblem4  22614  m2detleib  22615  indiscld  23075  xpstopnlem1  23793  xpstopnlem2  23795  ehl2eudis  25408  i1f1lem  25675  i1f1  25676  aannenlem2  26314  taylthlem2  26358  ppiublem2  27185  lgsdir2lem3  27309  ltsres  27645  noextendgt  27653  nolesgn2ores  27655  nosepnelem  27662  nosepdmlem  27666  nolt02o  27678  nosupno  27686  nosupbnd1lem3  27693  nosupbnd1  27697  nosupbnd2lem1  27698  noetainflem1  27720  ecgrtg  29071  elntg  29072  usgr2trlncl  29847  usgrwwlks2on  30045  umgrwwlks2on  30046  wlk2v2e  30246  eulerpathpr  30329  ex-br  30520  ex-eprel  30522  s2rnOLD  33024  trsp2cyc  33205  cyc3fv2  33220  esplyfvaln  33767  constrconj  33938  nn0constr  33954  subfacp1lem3  35419  kur14lem7  35449  ex-sategoelel12  35664  onpsstopbas  36667  onint1  36686  bj-inftyexpidisj  37579  kelac2  43519  omnord1ex  43758  oege2  43761  oenord1ex  43769  oenord1  43770  oaomoencom  43771  oenassex  43772  omcl3g  43788  onnoxp  43886  fvrcllb1d  44148  relexp1idm  44167  corcltrcl  44192  cotrclrcl  44195  clsk1indlem1  44498  mnuprdlem2  44726  mnuprdlem3  44727  mnurndlem1  44734  refsum2cnlem1  45494  limsup10exlem  46223  fourierdlem103  46660  fourierdlem104  46661  ioorrnopn  46756  ioorrnopnxr  46758  stgr1  48460  grlimgrtrilem1  48500  gpgiedgdmellem  48545  gpgvtx1  48553  gpg3kgrtriex  48588  pglem  48590  gpgprismgr4cycllem3  48596  gpgprismgr4cycllem9  48602  grlimedgnedg  48630  zlmodzxzscm  48856  zlmodzxzldeplem3  49001  nn0sumshdiglemB  49119  2arympt  49148  rrx2pyel  49211  rrx2linesl  49242  2sphere0  49249  termc2  50016