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

Theorem prid1g 4238
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 2609 . . 3 𝐴 = 𝐴
21orci 403 . 2 (𝐴 = 𝐴𝐴 = 𝐵)
3 elprg 4143 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴𝐴 = 𝐵)))
42, 3mpbiri 246 1 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381   = wceq 1474  wcel 1976  {cpr 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-sn 4125  df-pr 4127
This theorem is referenced by:  prid2g  4239  prid1  4240  prnzg  4253  preq1b  4312  elpreqprb  4330  opth1  4864  fr2nr  5006  fpr2g  6358  f1prex  6417  fveqf1o  6435  pw2f1olem  7926  hashprdifel  12999  gcdcllem3  15007  mgm2nsgrplem1  17174  mgm2nsgrplem2  17175  mgm2nsgrplem3  17176  sgrp2nmndlem1  17179  sgrp2rid2  17182  pmtrprfv  17642  pptbas  20564  coseq0negpitopi  23976  usgra2edg  25677  nbgraf1olem1  25736  nbgraf1olem3  25738  nbgraf1olem5  25740  nb3graprlem1  25746  nb3graprlem2  25747  constr1trl  25884  vdgr1b  26197  vdusgra0nedg  26201  usgravd0nedg  26211  vdn0frgrav2  26316  vdgn0frgrav2  26317  ftc1anclem8  32465  kelac2  36456  fourierdlem54  38857  sge0pr  39091  fmtnoprmfac2lem1  39821  imarnf1pr  40142  uhgr2edg  40437  umgrvad2edg  40442  uspgr2v1e2w  40479  usgr2v1e2w  40480  nbusgredgeu0  40598  nbusgrf1o0  40599  nb3grprlem1  40610  nb3grprlem2  40611  vtxduhgr0nedg  40709  1hegrlfgr  40724  1hegrvtxdg1  40725  1egrvtxdg1  40727  umgr2v2evd2  40745  vdegp1bi-av  40755
  Copyright terms: Public domain W3C validator