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

Theorem prid2 4455
Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Note: the proof from prid2g 4453 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 4454 . 2 𝐵 ∈ {𝐵, 𝐴}
3 prcom 4424 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
42, 3eleqtri 2842 1 𝐵 ∈ {𝐴, 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  Vcvv 3350  {cpr 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739  df-sn 4337  df-pr 4339
This theorem is referenced by:  prel12OLD  4536  opi2  5095  opeluu  5096  opthwiener  5137  dmrnssfld  5555  funopg  6104  2dom  8235  djuss  8999  dfac2b  9206  dfac2OLD  9208  brdom7disj  9608  brdom6disj  9609  cnelprrecn  10284  mnfxr  10352  m1expcl2  13092  hash2prb  13458  pr2pwpr  13465  sadcf  15459  xpsfrnel2  16494  setcepi  17006  grpss  17710  efgi1  18401  frgpuptinv  18453  dmdprdpr  18718  dprdpr  18719  cnmsgnsubg  20198  m2detleiblem6  20712  m2detleiblem3  20715  m2detleiblem4  20716  m2detleib  20717  indiscld  21178  xpstopnlem1  21895  xpstopnlem2  21897  i1f1lem  23750  i1f1  23751  aannenlem2  24378  taylthlem2  24422  ppiublem2  25222  lgsdir2lem3  25346  ecgrtg  26157  elntg  26158  usgr2trlncl  26951  umgrwwlks2on  27184  wlk2v2e  27438  eulerpathpr  27521  ex-br  27750  ex-eprel  27752  subfacp1lem3  31615  kur14lem7  31645  fprb  32117  sltres  32262  noextendgt  32270  nolesgn2ores  32272  nosepnelem  32277  nosepdmlem  32280  nolt02o  32292  nosupno  32296  nosupbnd1lem3  32303  nosupbnd1  32307  nosupbnd2lem1  32308  onpsstopbas  32871  onint1  32890  bj-inftyexpidisj  33534  kelac2  38315  fvrcllb1d  38665  relexp1idm  38684  corcltrcl  38709  cotrclrcl  38712  clsk1indlem1  39020  refsum2cnlem1  39851  limsup10exlem  40645  fourierdlem103  41066  fourierdlem104  41067  ioorrnopn  41165  ioorrnopnxr  41167  zlmodzxzscm  42807  zlmodzxzldeplem3  42963  nn0sumshdiglemB  43086
  Copyright terms: Public domain W3C validator