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

Theorem prid1 3638
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 3636 . 2  |-  ( A  e.  _V  ->  A  e.  { A ,  B } )
31, 2ax-mp 10 1  |-  A  e. 
{ A ,  B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2727   {cpr 3545
This theorem is referenced by:  prid2  3639  prnz  3649  preqr1  3686  preq12b  3688  prel12  3689  opi1  4133  unisn2  4413  opeluu  4417  dmrnssfld  4845  funopg  5144  fveqf1o  5658  2dom  6818  opthreg  7203  dfac2  7641  brdom7disj  8040  brdom6disj  8041  pnfxr  10334  m1expcl2  11003  sadcf  12518  prmreclem2  12838  xpsfrnel2  13341  setcepi  13764  grpss  14338  efgi0  14864  vrgpf  14912  vrgpinv  14913  frgpuptinv  14915  frgpup2  14920  frgpnabllem1  14996  dmdprdpr  15119  dprdpr  15120  indistopon  16570  indiscld  16660  xpstopnlem1  17332  xpstopnlem2  17334  xpsdsval  17777  i1f1lem  18876  i1f1  18877  dvf  19089  dvnfre  19133  dvmptcj  19149  dvmptre  19150  dvmptim  19151  rolle  19169  cmvth  19170  mvth  19171  dvlip  19172  dvlipcn  19173  c1lip2  19177  dvle  19186  dvivthlem1  19187  dvivth  19189  lhop2  19194  dvcnvre  19198  dvfsumle  19200  dvfsumge  19201  dvfsumabs  19202  dvfsumlem2  19206  dvfsum2  19213  ftc2  19223  itgparts  19226  itgsubstlem  19227  aannenlem2  19541  aalioulem3  19546  taylthlem2  19585  taylth  19586  efcvx  19657  pige3  19717  dvrelog  19816  advlog  19833  advlogexp  19834  logccv  19842  dvcxp1  19950  loglesqr  19966  divsqrsumlem  20106  ppiublem2  20274  logexprlim  20296  lgsdir2lem3  20396  logdivsum  20514  log2sumbnd  20525  subfacp1lem3  22884  kur14lem7  22914  eupath  23076  fprb  23297  noxp1o  23487  axfelem10  23523  onint1  24062  toplat  24456  pfsubkl  25213  pw2f1ocnv  26296  cnmsgnsubg  26600  lhe4.4ex1a  26712
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-sn 3550  df-pr 3551
  Copyright terms: Public domain W3C validator