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

Theorem prid1g 4077
 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 2450 . . 3
21orci 392 . 2
3 elprg 3983 . 2
42, 3mpbiri 237 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 370   wceq 1443   wcel 1886  cpr 3969 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-un 3408  df-sn 3968  df-pr 3970 This theorem is referenced by:  prid2g  4078  prid1  4079  preq1b  4145  elpreqprb  4161  opth1  4674  fr2nr  4811  fpr2g  6123  f1prex  6180  fveqf1o  6198  pw2f1olem  7673  hashprdifel  12572  gcdcllem3  14468  mgm2nsgrplem1  16645  mgm2nsgrplem2  16646  mgm2nsgrplem3  16647  sgrp2nmndlem1  16650  sgrp2rid2  16653  pmtrprfv  17087  pptbas  20016  coseq0negpitopi  23451  usgra2edg  25102  nbgraf1olem1  25162  nbgraf1olem3  25164  nbgraf1olem5  25166  nb3graprlem1  25172  nb3graprlem2  25173  constr1trl  25311  vdgr1b  25625  vdusgra0nedg  25629  usgravd0nedg  25639  vdn0frgrav2  25744  vdgn0frgrav2  25745  ftc1anclem8  32017  kelac2  35917  fourierdlem54  38018  sge0pr  38230  imarnf1pr  39010  usgr2edg  39277  nbusgredgeu0  39425  nbusgrf1o0  39426  nb3grprlem1  39437  nb3grprlem2  39438  vtxduhgr0nedg  39529  umgr2v2evd2  39547  usgvad2edg  39710
 Copyright terms: Public domain W3C validator