Theorem prid1 4297

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 4295	. 2 |- ( A e. _V -> A e. { A , B } )
3	1, 2	ax-mp 5	1 |- A e. { A , B }

Syntax hints:   e. wcel 1990   _Vcvv 3200   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  prid2  4298  prnz  4310  preqr1OLD  4380  preq12b  4382  prel12  4383  unisn2  4794  opi1  4937  opeluu  4939  dmrnssfld  5384  funopg  5922  fveqf1o  6557  2dom  8029  opthreg  8515  dfac2  8953  brdom7disj  9353  brdom6disj  9354  reelprrecn  10028  pnfxr  10092  m1expcl2  12882  hash2prb  13254  sadcf  15175  prmreclem2  15621  xpsfrnel2  16225  setcepi  16738  grpss  17440  efgi0  18133  vrgpf  18181  vrgpinv  18182  frgpuptinv  18184  frgpup2  18189  frgpnabllem1  18276  dmdprdpr  18448  dprdpr  18449  cnmsgnsubg  19923  m2detleiblem5  20431  m2detleiblem3  20435  m2detleiblem4  20436  m2detleib  20437  indistopon  20805  indiscld  20895  xpstopnlem1  21612  xpstopnlem2  21614  xpsdsval  22186  i1f1lem  23456  i1f1  23457  dvnfre  23715  c1lip2  23761  aannenlem2  24084  cxplogb  24524  ppiublem2  24928  lgsdir2lem3  25052  eengbas  25861  ebtwntg  25862  structvtxval  25910  usgr2trlncl  26656  umgrwwlks2on  26850  wlk2v2e  27017  eulerpathpr  27100  psgnid  29847  prsiga  30194  coinflippvt  30546  subfacp1lem3  31164  kur14lem7  31194  fprb  31669  noxp1o  31816  noextendlt  31822  nosepdmlem  31833  nolt02o  31845  nosupbnd1lem5  31858  nosupbnd2lem1  31861  noetalem1  31863  onint1  32448  poimirlem22  33431  pw2f1ocnv  37604  fvrcllb0d  37985  fvrcllb0da  37986  corclrcl  37999  relexp0idm  38007  corcltrcl  38031  refsum2cnlem1  39196  limsup10exlem  40004  fourierdlem103  40426  fourierdlem104  40427  prsal  40538  zlmodzxzscm  42135  zlmodzxzldeplem3  42291