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

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

Proof of Theorem prid1
StepHypRef Expression
1 prid1.1 . 2  |-  A  e. 
_V
2 prid1g 3732 . 2  |-  ( A  e.  _V  ->  A  e.  { A ,  B } )
31, 2ax-mp 8 1  |-  A  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   {cpr 3641
This theorem is referenced by:  prid2  3735  prnz  3745  preqr1  3786  preq12b  3788  prel12  3789  opi1  4240  unisn2  4522  opeluu  4526  dmrnssfld  4938  funopg  5286  fveqf1o  5806  2dom  6933  opthreg  7319  dfac2  7757  brdom7disj  8156  brdom6disj  8157  pnfxr  10455  m1expcl2  11125  sadcf  12644  prmreclem2  12964  xpsfrnel2  13467  setcepi  13920  grpss  14503  efgi0  15029  vrgpf  15077  vrgpinv  15078  frgpuptinv  15080  frgpup2  15085  frgpnabllem1  15161  dmdprdpr  15284  dprdpr  15285  indistopon  16738  indiscld  16828  xpstopnlem1  17500  xpstopnlem2  17502  xpsdsval  17945  i1f1lem  19044  i1f1  19045  dvf  19257  dvnfre  19301  dvmptcj  19317  dvmptre  19318  dvmptim  19319  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  c1lip2  19345  dvle  19354  dvivthlem1  19355  dvivth  19357  lhop2  19362  dvcnvre  19366  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  dvfsum2  19381  ftc2  19391  itgparts  19394  itgsubstlem  19395  aannenlem2  19709  aalioulem3  19714  taylthlem2  19753  taylth  19754  efcvx  19825  pige3  19885  dvrelog  19984  advlog  20001  advlogexp  20002  logccv  20010  dvcxp1  20082  loglesqr  20098  divsqrsumlem  20274  ppiublem2  20442  logexprlim  20464  lgsdir2lem3  20564  logdivsum  20682  log2sumbnd  20693  subfacp1lem3  23124  kur14lem7  23154  eupath  23316  fprb  23540  noxp1o  23731  nobnddown  23766  onint1  24299  dvreasin  24334  dvreacos  24335  areacirclem2  24337  areacirclem3  24338  toplat  24702  pfsubkl  25459  pw2f1ocnv  26542  cnmsgnsubg  26846  lhe4.4ex1a  26958  refsum2cnlem1  27120  dvcosre  27153  itgsin0pilem1  27156  itgsinexplem1  27160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator