MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prid2 Structured version   Visualization version   GIF version

Theorem prid2 4693
Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4691 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
StepHypRef Expression
1 prid2.1 . . 3 𝐵 ∈ V
21prid1 4692 . 2 𝐵 ∈ {𝐵, 𝐴}
3 prcom 4662 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
42, 3eleqtri 2911 1 𝐵 ∈ {𝐴, 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3495  {cpr 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3940  df-sn 4560  df-pr 4562
This theorem is referenced by:  opi2  5353  opeluu  5354  opthwiener  5396  dmrnssfld  5835  funopg  6383  fprb  6949  2dom  8571  djuss  9338  dfac2b  9545  brdom7disj  9942  brdom6disj  9943  cnelprrecn  10619  mnfxr  10687  seqexw  13375  m1expcl2  13441  hash2prb  13820  pr2pwpr  13827  sadcf  15792  fnpr2ob  16821  setcepi  17338  grpss  18061  efgi1  18778  frgpuptinv  18828  dmdprdpr  19102  dprdpr  19103  cnmsgnsubg  20651  m2detleiblem6  21165  m2detleiblem3  21168  m2detleiblem4  21169  m2detleib  21170  indiscld  21629  xpstopnlem1  22347  xpstopnlem2  22349  ehl2eudis  23954  i1f1lem  24219  i1f1  24220  aannenlem2  24847  taylthlem2  24891  ppiublem2  25707  lgsdir2lem3  25831  ecgrtg  26697  elntg  26698  usgr2trlncl  27469  umgrwwlks2on  27664  wlk2v2e  27864  eulerpathpr  27947  ex-br  28138  ex-eprel  28140  s2rn  30548  trsp2cyc  30693  cyc3fv2  30708  subfacp1lem3  32327  kur14lem7  32357  ex-sategoelel12  32572  sltres  33067  noextendgt  33075  nolesgn2ores  33077  nosepnelem  33082  nosepdmlem  33085  nolt02o  33097  nosupno  33101  nosupbnd1lem3  33108  nosupbnd1  33112  nosupbnd2lem1  33113  onpsstopbas  33676  onint1  33695  bj-inftyexpidisj  34385  kelac2  39545  fvrcllb1d  39920  relexp1idm  39939  corcltrcl  39964  cotrclrcl  39967  clsk1indlem1  40275  mnuprdlem2  40489  mnuprdlem3  40490  mnurndlem1  40497  refsum2cnlem1  41174  limsup10exlem  41933  fourierdlem103  42375  fourierdlem104  42376  ioorrnopn  42471  ioorrnopnxr  42473  zlmodzxzscm  44303  zlmodzxzldeplem3  44455  nn0sumshdiglemB  44578  rrx2pyel  44597  rrx2linesl  44628  2sphere0  44635
  Copyright terms: Public domain W3C validator