Theorem prid2 4702

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

Syntax hints:   ∈ wcel 2113  Vcvv 3497  {cpr 4572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-un 3944  df-sn 4571  df-pr 4573

This theorem is referenced by:  opi2  5364  opeluu  5365  opthwiener  5407  dmrnssfld  5844  funopg  6392  fprb  6959  2dom  8585  djuss  9352  dfac2b  9559  brdom7disj  9956  brdom6disj  9957  cnelprrecn  10633  mnfxr  10701  seqexw  13388  m1expcl2  13454  hash2prb  13833  pr2pwpr  13840  sadcf  15805  fnpr2ob  16834  setcepi  17351  grpss  18124  efgi1  18850  frgpuptinv  18900  dmdprdpr  19174  dprdpr  19175  cnmsgnsubg  20724  m2detleiblem6  21238  m2detleiblem3  21241  m2detleiblem4  21242  m2detleib  21243  indiscld  21702  xpstopnlem1  22420  xpstopnlem2  22422  ehl2eudis  24028  i1f1lem  24293  i1f1  24294  aannenlem2  24921  taylthlem2  24965  ppiublem2  25782  lgsdir2lem3  25906  ecgrtg  26772  elntg  26773  usgr2trlncl  27544  umgrwwlks2on  27739  wlk2v2e  27939  eulerpathpr  28022  ex-br  28213  ex-eprel  28215  s2rn  30624  trsp2cyc  30769  cyc3fv2  30784  subfacp1lem3  32433  kur14lem7  32463  ex-sategoelel12  32678  sltres  33173  noextendgt  33181  nolesgn2ores  33183  nosepnelem  33188  nosepdmlem  33191  nolt02o  33203  nosupno  33207  nosupbnd1lem3  33214  nosupbnd1  33218  nosupbnd2lem1  33219  onpsstopbas  33782  onint1  33801  bj-inftyexpidisj  34496  kelac2  39671  fvrcllb1d  40046  relexp1idm  40065  corcltrcl  40090  cotrclrcl  40093  clsk1indlem1  40401  mnuprdlem2  40615  mnuprdlem3  40616  mnurndlem1  40623  refsum2cnlem1  41300  limsup10exlem  42059  fourierdlem103  42501  fourierdlem104  42502  ioorrnopn  42597  ioorrnopnxr  42599  zlmodzxzscm  44412  zlmodzxzldeplem3  44564  nn0sumshdiglemB  44687  rrx2pyel  44706  rrx2linesl  44737  2sphere0  44744