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

Theorem prid1g 4763
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 2733 . . 3 𝐴 = 𝐴
21orci 864 . 2 (𝐴 = 𝐴𝐴 = 𝐵)
3 elprg 4648 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
42, 3mpbiri 258 1 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846   = wceq 1542  wcel 2107  {cpr 4629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3952  df-sn 4628  df-pr 4630
This theorem is referenced by:  prid2g  4764  prid1  4765  prnzg  4781  preq1b  4846  prel12g  4863  elpreqprb  4867  prproe  4905  opth1  5474  fr2nr  5653  fpr2g  7208  f1prex  7277  fveqf1o  7296  pw2f1olem  9072  hashprdifel  14354  gcdcllem3  16438  mgm2nsgrplem1  18795  mgm2nsgrplem2  18796  mgm2nsgrplem3  18797  sgrp2nmndlem1  18800  sgrp2rid2  18803  pmtrprfv  19314  pptbas  22493  coseq0negpitopi  25995  uhgr2edg  28445  umgrvad2edg  28450  uspgr2v1e2w  28488  usgr2v1e2w  28489  nbusgredgeu0  28605  nbusgrf1o0  28606  nb3grprlem1  28617  nb3grprlem2  28618  vtxduhgr0nedg  28729  1hegrvtxdg1  28744  1egrvtxdg1  28746  umgr2v2evd2  28764  vdegp1bi  28774  mptprop  31898  altgnsg  32286  cyc3genpmlem  32288  elrspunsn  32505  bj-prmoore  35934  ftc1anclem8  36506  kelac2  41740  pr2el1  42233  pr2eldif1  42238  fourierdlem54  44811  sge0pr  45045  imarnf1pr  45925  paireqne  46114  fmtnoprmfac2lem1  46169  1hegrlfgr  46445
  Copyright terms: Public domain W3C validator