Theorem prid1 4716

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	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
prid1	⊢ 𝐴 ∈ {𝐴, 𝐵}

Proof of Theorem prid1

Step	Hyp	Ref	Expression
1		prid1.1	. 2 ⊢ 𝐴 ∈ V
2		prid1g 4714	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2113  Vcvv 3437  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580

This theorem is referenced by:  prid2  4717  prnz  4731  preq12b  4803  unisn2  5254  opi1  5413  opeluu  5415  dmrnssfld  5919  funopg  6522  fprb  7136  fveqf1o  7244  2dom  8961  dif1en  9080  opthreg  9517  djuss  9822  dfac2b  10031  brdom7disj  10431  brdom6disj  10432  reelprrecn  11107  pnfxr  11175  m1expcl2  13996  hash2prb  14383  sadcf  16368  prmreclem2  16833  fnpr2ob  17466  setcepi  17999  setc2obas  18005  setc2ohom  18006  cat1  18008  grpss  18871  efgi0  19636  vrgpf  19684  vrgpinv  19685  frgpuptinv  19687  frgpup2  19692  frgpnabllem1  19789  dmdprdpr  19967  dprdpr  19968  cnmsgnsubg  21518  m2detleiblem5  22543  m2detleiblem3  22547  m2detleiblem4  22548  m2detleib  22549  indistopon  22919  indiscld  23009  xpstopnlem1  23727  xpstopnlem2  23729  xpsdsval  24299  ehl2eudis  25352  i1f1lem  25620  i1f1  25621  dvnfre  25886  c1lip2  25933  aannenlem2  26267  cxplogb  26726  ppiublem2  27144  lgsdir2lem3  27268  noxp1o  27605  noextendlt  27611  nosepdmlem  27625  nolt02o  27637  nosupbnd1lem5  27654  nosupbnd2lem1  27657  noinfno  27660  noinfbnd1  27671  noinfbnd2lem1  27672  noetasuplem1  27675  eengbas  28963  ebtwntg  28964  structvtxval  29003  usgr2trlncl  29742  usgrwwlks2on  29940  umgrwwlks2on  29941  wlk2v2e  30141  eulerpathpr  30224  s2rnOLD  32934  psgnid  33075  trsp2cyc  33101  cyc3fv1  33115  cnmsgn0g  33124  constr01  33778  constrss  33779  constrconj  33781  constrelextdg2  33783  nn0constr  33797  prsiga  34167  coinflippvt  34521  subfacp1lem3  35249  kur14lem7  35279  ex-sategoelel12  35494  onint1  36516  poimirlem22  37705  pw2f1ocnv  43157  2omomeqom  43423  omcl3g  43454  fvrcllb0d  43813  fvrcllb0da  43814  corclrcl  43827  relexp0idm  43835  corcltrcl  43859  mnuprdlem1  44392  mnuprdlem3  44394  mnurndlem1  44401  nregmodellem  45136  refsum2cnlem1  45161  limsup10exlem  45897  fourierdlem103  46334  fourierdlem104  46335  prsal  46443  usgrgrtrirex  48077  stgr1  48088  stgrnbgr0  48091  grlimgrtrilem1  48128  gpgiedgdmellem  48173  gpgvtx0  48180  gpgprismgr4cycllem3  48224  gpgprismgr4cycllem9  48230  zlmodzxzscm  48484  zlmodzxzldeplem3  48630  2arympt  48777  rrx2pxel  48839  rrx2linesl  48871  2sphere0  48878  setc1onsubc  49730