Theorem prid2 4606

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

Syntax hints:   ∈ wcel 2081  Vcvv 3437  {cpr 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-un 3864  df-sn 4473  df-pr 4475

This theorem is referenced by:  opi2  5253  opeluu  5254  opthwiener  5295  dmrnssfld  5722  funopg  6259  fprb  6823  2dom  8430  djuss  9195  dfac2b  9402  brdom7disj  9799  brdom6disj  9800  cnelprrecn  10476  mnfxr  10545  seqexw  13235  m1expcl2  13301  hash2prb  13676  pr2pwpr  13683  sadcf  15635  fnpr2ob  16660  setcepi  17177  grpss  17879  efgi1  18574  frgpuptinv  18624  dmdprdpr  18888  dprdpr  18889  cnmsgnsubg  20403  m2detleiblem6  20919  m2detleiblem3  20922  m2detleiblem4  20923  m2detleib  20924  indiscld  21383  xpstopnlem1  22101  xpstopnlem2  22103  ehl2eudis  23708  i1f1lem  23973  i1f1  23974  aannenlem2  24601  taylthlem2  24645  ppiublem2  25461  lgsdir2lem3  25585  ecgrtg  26452  elntg  26453  usgr2trlncl  27228  umgrwwlks2on  27423  wlk2v2e  27623  eulerpathpr  27707  ex-br  27902  ex-eprel  27904  s2rn  30300  trsp2cyc  30412  cyc3fv2  30417  subfacp1lem3  32037  kur14lem7  32067  ex-sategoelel12  32282  sltres  32778  noextendgt  32786  nolesgn2ores  32788  nosepnelem  32793  nosepdmlem  32796  nolt02o  32808  nosupno  32812  nosupbnd1lem3  32819  nosupbnd1  32823  nosupbnd2lem1  32824  onpsstopbas  33387  onint1  33406  bj-inftyexpidisj  34050  kelac2  39150  fvrcllb1d  39525  relexp1idm  39544  corcltrcl  39569  cotrclrcl  39572  clsk1indlem1  39880  mnuprdlem2  40106  mnuprdlem3  40107  mnurndlem1  40114  refsum2cnlem1  40833  limsup10exlem  41595  fourierdlem103  42036  fourierdlem104  42037  ioorrnopn  42132  ioorrnopnxr  42134  zlmodzxzscm  43883  zlmodzxzldeplem3  44037  nn0sumshdiglemB  44161  rrx2pyel  44180  rrx2linesl  44211  2sphere0  44218