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

Theorem prid2 3881
Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
prid2.1  |-  B  e. 
_V
Assertion
Ref Expression
prid2  |-  B  e. 
{ A ,  B }

Proof of Theorem prid2
StepHypRef Expression
1 prid2.1 . . 3  |-  B  e. 
_V
21prid1 3880 . 2  |-  B  e. 
{ B ,  A }
3 prcom 3850 . 2  |-  { B ,  A }  =  { A ,  B }
42, 3eleqtri 2484 1  |-  B  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2924   {cpr 3783
This theorem is referenced by:  prel12  3943  opi2  4399  opthwiener  4426  opeluu  4682  dmrnssfld  5096  funopg  5452  2dom  7146  dfac2  7975  brdom7disj  8373  brdom6disj  8374  mnfxr  10678  m1expcl2  11366  sadcf  12928  xpsfrnel2  13753  setcepi  14206  grpss  14789  efgi1  15316  frgpuptinv  15366  dmdprdpr  15570  dprdpr  15571  indiscld  17118  xpstopnlem1  17802  xpstopnlem2  17804  i1f1lem  19542  i1f1  19543  dvfcn  19756  dvnres  19778  dvexp  19800  dvexp3  19823  dvef  19825  dvsincos  19826  dvlipcn  19839  dv11cn  19846  dvply1  20162  aannenlem2  20207  dvtaylp  20247  taylthlem2  20251  pserdvlem2  20305  pige3  20386  dvlog  20503  advlogexp  20507  logtayl  20512  dvcxp1  20587  dvcxp2  20588  dvatan  20736  efrlim  20769  ppiublem2  20948  lgsdir2lem3  21070  logdivsum  21188  log2sumbnd  21199  wlkntrl  21523  constr3lem4  21595  eupath  21664  ex-br  21700  ex-eprel  21702  lgamgulmlem2  24775  subfacp1lem3  24829  kur14lem7  24859  fprb  25351  sltres  25540  noxp2o  25543  nobndup  25576  onpsstopbas  26092  onint1  26111  dvreasin  26187  kelac2  27039  cnmsgnsubg  27310  lhe4.4ex1a  27422  expgrowthi  27426  expgrowth  27428  refsum2cnlem1  27583  dvsinexp  27615  usgra2pthspth  28043  usgra2wlkspthlem2  28045  usg2wlkonot  28088  usg2wotspth  28089
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-un 3293  df-sn 3788  df-pr 3789
  Copyright terms: Public domain W3C validator