Theorem prid1 4691

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 4689	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2113  Vcvv 3491  {cpr 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-v 3493  df-un 3934  df-sn 4561  df-pr 4563

This theorem is referenced by:  prid2  4692  prnz  4705  preq12b  4774  unisn2  5209  opi1  5353  opeluu  5355  dmrnssfld  5834  funopg  6382  fprb  6949  fveqf1o  7051  2dom  8575  opthreg  9074  djuss  9342  dfac2b  9549  brdom7disj  9946  brdom6disj  9947  reelprrecn  10622  pnfxr  10688  m1expcl2  13448  hash2prb  13827  sadcf  15795  prmreclem2  16246  fnpr2ob  16824  setcepi  17341  grpss  18114  efgi0  18839  vrgpf  18887  vrgpinv  18888  frgpuptinv  18890  frgpup2  18895  frgpnabllem1  18986  dmdprdpr  19164  dprdpr  19165  cnmsgnsubg  20714  m2detleiblem5  21227  m2detleiblem3  21231  m2detleiblem4  21232  m2detleib  21233  indistopon  21602  indiscld  21692  xpstopnlem1  22410  xpstopnlem2  22412  xpsdsval  22984  ehl2eudis  24018  i1f1lem  24283  i1f1  24284  dvnfre  24544  c1lip2  24590  aannenlem2  24914  cxplogb  25360  ppiublem2  25775  lgsdir2lem3  25899  eengbas  26763  ebtwntg  26764  structvtxval  26802  usgr2trlncl  27537  umgrwwlks2on  27732  wlk2v2e  27932  eulerpathpr  28015  s2rn  30618  psgnid  30758  trsp2cyc  30784  cyc3fv1  30798  cnmsgn0g  30807  prsiga  31409  coinflippvt  31761  subfacp1lem3  32448  kur14lem7  32478  ex-sategoelel12  32693  noxp1o  33189  noextendlt  33195  nosepdmlem  33206  nolt02o  33218  nosupbnd1lem5  33231  nosupbnd2lem1  33234  noetalem1  33236  onint1  33816  poimirlem22  34956  pw2f1ocnv  39717  fvrcllb0d  40119  fvrcllb0da  40120  corclrcl  40133  relexp0idm  40141  corcltrcl  40165  mnuprdlem1  40689  mnuprdlem3  40691  mnurndlem1  40698  refsum2cnlem1  41375  limsup10exlem  42134  fourierdlem103  42575  fourierdlem104  42576  prsal  42684  zlmodzxzscm  44481  zlmodzxzldeplem3  44633  rrx2pxel  44774  rrx2linesl  44806  2sphere0  44813