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

Theorem prid1g 4688
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 2818 . . 3 𝐴 = 𝐴
21orci 859 . 2 (𝐴 = 𝐴𝐴 = 𝐵)
3 elprg 4578 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
42, 3mpbiri 259 1 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841   = wceq 1528  wcel 2105  {cpr 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-sn 4558  df-pr 4560
This theorem is referenced by:  prid2g  4689  prid1  4690  prnzg  4705  preq1b  4769  prel12g  4786  elpreqprb  4790  prproe  4828  opth1  5358  fr2nr  5526  fpr2g  6965  f1prex  7031  fveqf1o  7049  pw2f1olem  8609  hashprdifel  13747  gcdcllem3  15838  mgm2nsgrplem1  18021  mgm2nsgrplem2  18022  mgm2nsgrplem3  18023  sgrp2nmndlem1  18026  sgrp2rid2  18029  pmtrprfv  18510  pptbas  21544  coseq0negpitopi  25016  uhgr2edg  26917  umgrvad2edg  26922  uspgr2v1e2w  26960  usgr2v1e2w  26961  nbusgredgeu0  27077  nbusgrf1o0  27078  nb3grprlem1  27089  nb3grprlem2  27090  vtxduhgr0nedg  27201  1hegrvtxdg1  27216  1egrvtxdg1  27218  umgr2v2evd2  27236  vdegp1bi  27246  mptprop  30360  altgnsg  30718  cyc3genpmlem  30720  ftc1anclem8  34855  kelac2  39543  pr2el1  39786  pr2eldif1  39791  fourierdlem54  42322  sge0pr  42553  imarnf1pr  43358  paireqne  43550  fmtnoprmfac2lem1  43605  1hegrlfgr  43884
  Copyright terms: Public domain W3C validator