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

Theorem prid1 3880
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 3878 . 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 1721   _Vcvv 2924   {cpr 3783
This theorem is referenced by:  prid2  3881  prnz  3891  preqr1  3940  preq12b  3942  prel12  3943  opi1  4398  unisn2  4678  opeluu  4682  dmrnssfld  5096  funopg  5452  fveqf1o  5996  2dom  7146  opthreg  7537  dfac2  7975  brdom7disj  8373  brdom6disj  8374  pnfxr  10677  m1expcl2  11366  sadcf  12928  prmreclem2  13248  xpsfrnel2  13753  setcepi  14206  grpss  14789  efgi0  15315  vrgpf  15363  vrgpinv  15364  frgpuptinv  15366  frgpup2  15371  frgpnabllem1  15447  dmdprdpr  15570  dprdpr  15571  indistopon  17028  indiscld  17118  xpstopnlem1  17802  xpstopnlem2  17804  xpsdsval  18372  i1f1lem  19542  i1f1  19543  dvf  19755  dvnfre  19799  dvmptcj  19815  dvmptre  19816  dvmptim  19817  rolle  19835  cmvth  19836  mvth  19837  dvlip  19838  dvlipcn  19839  c1lip2  19843  dvle  19852  dvivthlem1  19853  dvivth  19855  lhop2  19860  dvcnvre  19864  dvfsumle  19866  dvfsumge  19867  dvfsumabs  19868  dvfsumlem2  19872  dvfsum2  19879  ftc2  19889  itgparts  19892  itgsubstlem  19893  aannenlem2  20207  aalioulem3  20212  taylthlem2  20251  taylth  20252  efcvx  20326  pige3  20386  dvrelog  20489  advlog  20506  advlogexp  20507  logccv  20515  dvcxp1  20587  loglesqr  20603  divsqrsumlem  20779  ppiublem2  20948  logexprlim  20970  lgsdir2lem3  21070  logdivsum  21188  log2sumbnd  21199  wlkntrl  21523  constr3lem4  21595  eupath  21664  prsiga  24475  coinflippvt  24703  lgamgulmlem2  24775  subfacp1lem3  24829  kur14lem7  24859  fprb  25351  noxp1o  25542  nobnddown  25577  onint1  26111  dvreasin  26187  dvreacos  26188  areacirclem2  26189  areacirclem3  26190  pw2f1ocnv  27006  cnmsgnsubg  27310  lhe4.4ex1a  27422  refsum2cnlem1  27583  dvcosre  27616  itgsin0pilem1  27619  itgsinexplem1  27623  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