Theorem prid2 4139

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

Assertion

Ref	Expression
prid2

Proof of Theorem prid2

Step	Hyp	Ref	Expression
1		prid2.1	. . 3
2	1	prid1 4138	. 2
3		prcom 4108	. 2
4	2, 3	eleqtri 2543	1

Syntax hints:  e.wcel 1818  cvv 3109  {cpr 4031

This theorem is referenced by:  prel12  4207  opi2  4720  opeluu  4721  opthwiener  4754  dmrnssfld  5266  funopg  5625  2dom  7608  dfac2  8532  brdom7disj  8930  brdom6disj  8931  cnelprrecn  9606  mnfxr  11352  m1expcl2  12188  hash2prd  12518  pr2pwpr  12520  hash2prv  12525  hash2sspr  12526  sadcf  14103  xpsfrnel2  14962  setcepi  15415  grpss  16071  efgi1  16739  frgpuptinv  16789  dmdprdpr  17098  dprdpr  17099  cnmsgnsubg  18613  m2detleiblem6  19128  m2detleiblem3  19131  m2detleiblem4  19132  m2detleib  19133  indiscld  19592  xpstopnlem1  20310  xpstopnlem2  20312  i1f1lem  22096  i1f1  22097  aannenlem2  22725  taylthlem2  22769  ppiublem2  23478  lgsdir2lem3  23600  ecgrtg  24286  elntg  24287  wlkntrl  24564  usgra2wlkspthlem2  24620  constr3lem4  24647  usg2wlkonot  24883  usg2wotspth  24884  eupath  24981  ex-br  25152  ex-eprel  25154  subfacp1lem3  28626  kur14lem7  28656  fprb  29203  sltres  29424  noxp2o  29427  nobndup  29460  onpsstopbas  29895  onint1  29914  kelac2  31011  refsum2cnlem1  31412  fourierdlem103  31992  fourierdlem104  31993  usgra2pthspth  32351  zlmodzxzscm  32946  zlmodzxzldeplem3  33103  bj-inftyexpidisj  34613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032