Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prid1g Structured version   Visualization version   GIF version

Theorem prid1g 4327
 Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
Assertion
Ref Expression
prid1g (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})

Proof of Theorem prid1g
StepHypRef Expression
1 eqid 2651 . . 3 𝐴 = 𝐴
21orci 404 . 2 (𝐴 = 𝐴𝐴 = 𝐵)
3 elprg 4229 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
42, 3mpbiri 248 1 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382   = wceq 1523   ∈ wcel 2030  {cpr 4212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213 This theorem is referenced by:  prid2g  4328  prid1  4329  prnzg  4342  preq1b  4409  elpreqprb  4428  prproe  4466  opth1  4973  fr2nr  5121  fpr2g  6516  f1prex  6579  fveqf1o  6597  pw2f1olem  8105  hashprdifel  13224  gcdcllem3  15270  mgm2nsgrplem1  17452  mgm2nsgrplem2  17453  mgm2nsgrplem3  17454  sgrp2nmndlem1  17457  sgrp2rid2  17460  pmtrprfv  17919  pptbas  20860  coseq0negpitopi  24300  uhgr2edg  26145  umgrvad2edg  26150  uspgr2v1e2w  26188  usgr2v1e2w  26189  nbusgredgeu0  26314  nbusgrf1o0  26315  nb3grprlem1  26326  nb3grprlem2  26327  vtxduhgr0nedg  26444  1hegrvtxdg1  26459  1egrvtxdg1  26461  umgr2v2evd2  26479  vdegp1bi  26489  ftc1anclem8  33622  kelac2  37952  fourierdlem54  40695  sge0pr  40929  imarnf1pr  41624  fmtnoprmfac2lem1  41803  1hegrlfgr  42038
 Copyright terms: Public domain W3C validator