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

Theorem prid1 3914
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 3912 . 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 1726   _Vcvv 2958   {cpr 3817
This theorem is referenced by:  prid2  3915  prnz  3925  preqr1  3974  preq12b  3976  prel12  3977  opi1  4432  unisn2  4713  opeluu  4717  dmrnssfld  5131  funopg  5487  fveqf1o  6031  2dom  7181  opthreg  7575  dfac2  8013  brdom7disj  8411  brdom6disj  8412  pnfxr  10715  m1expcl2  11405  sadcf  12967  prmreclem2  13287  xpsfrnel2  13792  setcepi  14245  grpss  14828  efgi0  15354  vrgpf  15402  vrgpinv  15403  frgpuptinv  15405  frgpup2  15410  frgpnabllem1  15486  dmdprdpr  15609  dprdpr  15610  indistopon  17067  indiscld  17157  xpstopnlem1  17843  xpstopnlem2  17845  xpsdsval  18413  i1f1lem  19583  i1f1  19584  dvf  19796  dvnfre  19840  dvmptcj  19856  dvmptre  19857  dvmptim  19858  rolle  19876  cmvth  19877  mvth  19878  dvlip  19879  dvlipcn  19880  c1lip2  19884  dvle  19893  dvivthlem1  19894  dvivth  19896  lhop2  19901  dvcnvre  19905  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  dvfsumlem2  19913  dvfsum2  19920  ftc2  19930  itgparts  19933  itgsubstlem  19934  aannenlem2  20248  aalioulem3  20253  taylthlem2  20292  taylth  20293  efcvx  20367  pige3  20427  dvrelog  20530  advlog  20547  advlogexp  20548  logccv  20556  dvcxp1  20628  loglesqr  20644  divsqrsumlem  20820  ppiublem2  20989  logexprlim  21011  lgsdir2lem3  21111  logdivsum  21229  log2sumbnd  21240  wlkntrl  21564  constr3lem4  21636  eupath  21705  prsiga  24516  coinflippvt  24744  lgamgulmlem2  24816  subfacp1lem3  24870  kur14lem7  24900  fprb  25399  noxp1o  25623  nobnddown  25658  onint1  26201  ftc1anclem8  26289  ftc2nc  26291  dvreasin  26292  dvreacos  26293  areacirclem1  26294  pw2f1ocnv  27110  cnmsgnsubg  27413  lhe4.4ex1a  27525  refsum2cnlem1  27686  dvcosre  27719  itgsin0pilem1  27722  itgsinexplem1  27726  hash2prv  28181  hash2sspr  28182  usgra2wlkspthlem2  28333  usg2wlkonot  28403  usg2wotspth  28404
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-sn 3822  df-pr 3823
  Copyright terms: Public domain W3C validator