Theorem prid1 4135

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.)

Hypothesis

Ref	Expression
prid1.1	|- A e. _V

Assertion

Ref	Expression
prid1	|- A e. { A , B }

Proof of Theorem prid1

Step	Hyp	Ref	Expression
1		prid1.1	. 2 |- A e. _V
2		prid1g 4133	. 2 |- ( A e. _V -> A e. { A , B } )
3	1, 2	ax-mp 5	1 |- A e. { A , B }

Syntax hints:   e. wcel 1767   _Vcvv 3113   {cpr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030

This theorem is referenced by:  prid2  4136  prnz  4146  preqr1  4200  preq12b  4202  prel12  4203  unisn2  4583  opi1  4714  opeluu  4716  dmrnssfld  5261  funopg  5620  fveqf1o  6193  2dom  7588  opthreg  8035  dfac2  8511  brdom7disj  8909  brdom6disj  8910  reelprrecn  9584  pnfxr  11321  m1expcl2  12156  hash2prd  12484  hash2prv  12491  hash2sspr  12492  sadcf  13962  prmreclem2  14294  xpsfrnel2  14820  setcepi  15273  grpss  15881  efgi0  16544  vrgpf  16592  vrgpinv  16593  frgpuptinv  16595  frgpup2  16600  frgpnabllem1  16680  dmdprdpr  16900  dprdpr  16901  cnmsgnsubg  18408  m2detleiblem5  18922  m2detleiblem3  18926  m2detleiblem4  18927  m2detleib  18928  indistopon  19296  indiscld  19386  xpstopnlem1  20073  xpstopnlem2  20075  xpsdsval  20647  i1f1lem  21859  i1f1  21860  dvnfre  22118  c1lip2  22162  aannenlem2  22487  ppiublem2  23234  lgsdir2lem3  23356  eengbas  23988  ebtwntg  23989  wlkntrl  24268  usgra2wlkspthlem2  24324  constr3lem4  24351  usg2wlkonot  24587  usg2wotspth  24588  eupath  24685  prsiga  27799  coinflippvt  28091  subfacp1lem3  28294  kur14lem7  28324  fprb  28808  noxp1o  29031  nobnddown  29066  onint1  29519  pw2f1ocnv  30611  refsum2cnlem1  31018  dvcnre  31272  itgiccshift  31326  itgperiod  31327  itgsbtaddcnst  31328  dirkeritg  31430  dirkercncflem2  31432  fourierdlem28  31463  fourierdlem39  31474  fourierdlem56  31491  fourierdlem57  31492  fourierdlem58  31493  fourierdlem59  31494  fourierdlem60  31495  fourierdlem61  31496  fourierdlem62  31497  fourierdlem68  31503  fourierdlem72  31507  fourierdlem103  31538  fourierdlem104  31539  zlmodzxzscm  32042  zlmodzxzldeplem3  32202