Theorem prid1 4123

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

Syntax hints:   e. wcel 1804   _Vcvv 3095   {cpr 4016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017

This theorem is referenced by:  prid2  4124  prnz  4134  preqr1  4189  preq12b  4191  prel12  4192  unisn2  4573  opi1  4704  opeluu  4706  dmrnssfld  5251  funopg  5610  fveqf1o  6190  2dom  7590  opthreg  8038  dfac2  8514  brdom7disj  8912  brdom6disj  8913  reelprrecn  9587  pnfxr  11331  m1expcl2  12169  hash2prd  12499  hash2prv  12506  hash2sspr  12507  sadcf  14084  prmreclem2  14416  xpsfrnel2  14943  setcepi  15393  grpss  16049  efgi0  16716  vrgpf  16764  vrgpinv  16765  frgpuptinv  16767  frgpup2  16772  frgpnabllem1  16855  dmdprdpr  17076  dprdpr  17077  cnmsgnsubg  18590  m2detleiblem5  19104  m2detleiblem3  19108  m2detleiblem4  19109  m2detleib  19110  indistopon  19479  indiscld  19569  xpstopnlem1  20287  xpstopnlem2  20289  xpsdsval  20861  i1f1lem  22073  i1f1  22074  dvnfre  22332  c1lip2  22376  aannenlem2  22701  ppiublem2  23454  lgsdir2lem3  23576  eengbas  24260  ebtwntg  24261  wlkntrl  24540  usgra2wlkspthlem2  24596  constr3lem4  24623  usg2wlkonot  24859  usg2wotspth  24860  eupath  24957  prsiga  28108  coinflippvt  28400  subfacp1lem3  28603  kur14lem7  28633  fprb  29178  noxp1o  29401  nobnddown  29436  onint1  29889  pw2f1ocnv  30954  refsum2cnlem1  31366  fourierdlem103  31881  fourierdlem104  31882  zlmodzxzscm  32679  zlmodzxzldeplem3  32838