Theorem prid1 3971

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

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

Syntax hints:   e. wcel 1755   _Vcvv 2962   {cpr 3867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-sn 3866  df-pr 3868

This theorem is referenced by:  prid2  3972  prnz  3982  preqr1  4034  preq12b  4036  prel12  4037  unisn2  4416  opi1  4547  opeluu  4549  dmrnssfld  5085  funopg  5438  fveqf1o  5987  2dom  7370  opthreg  7812  dfac2  8288  brdom7disj  8686  brdom6disj  8687  reelprrecn  9362  pnfxr  11080  m1expcl2  11871  hash2prd  12165  sadcf  13632  prmreclem2  13961  xpsfrnel2  14486  setcepi  14939  grpss  15539  efgi0  16197  vrgpf  16245  vrgpinv  16246  frgpuptinv  16248  frgpup2  16253  frgpnabllem1  16331  dmdprdpr  16522  dprdpr  16523  cnmsgnsubg  17849  m2detleiblem5  18273  m2detleiblem3  18277  m2detleiblem4  18278  m2detleib  18279  indistopon  18447  indiscld  18537  xpstopnlem1  19224  xpstopnlem2  19226  xpsdsval  19798  i1f1lem  21009  i1f1  21010  dvnfre  21268  c1lip2  21312  aannenlem2  21680  ppiublem2  22427  lgsdir2lem3  22549  eengbas  23050  ebtwntg  23051  wlkntrl  23284  constr3lem4  23356  eupath  23425  prsiga  26428  coinflippvt  26715  subfacp1lem3  26918  kur14lem7  26948  fprb  27431  noxp1o  27654  nobnddown  27689  onint1  28143  pw2f1ocnv  29231  refsum2cnlem1  29604  hash2prv  30072  hash2sspr  30073  usgra2wlkspthlem2  30143  usg2wlkonot  30248  usg2wotspth  30249  zlmodzxzscm  30588  zlmodzxzldeplem3  30753