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

Theorem prid1g 4136
 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 2457 . . 3
21orci 390 . 2
3 elprg 4045 . 2
42, 3mpbiri 233 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  \/wo 368  =wceq 1395  e.wcel 1818  {cpr 4031 This theorem is referenced by:  prid2g  4137  prid1  4138  opth1  4725  fr2nr  4862  fveqf1o  6205  pw2f1olem  7641  hashprdifel  12463  gcdcllem3  14151  mgm2nsgrplem1  16036  mgm2nsgrplem2  16037  mgm2nsgrplem3  16038  sgrp2nmndlem1  16041  sgrp2rid2  16044  pmtrprfv  16478  pptbas  19509  coseq0negpitopi  22896  usgra2edg  24382  nbgraf1olem1  24441  nbgraf1olem3  24443  nbgraf1olem5  24445  nb3graprlem1  24451  nb3graprlem2  24452  constr1trl  24590  vdgr1b  24904  vdusgra0nedg  24908  usgravd0nedg  24918  vdn0frgrav2  25023  vdgn0frgrav2  25024  ftc1anclem8  30097  kelac2  31011  fourierdlem54  31943  imarnf1pr  32309  usgvad2edg  32411 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032
 Copyright terms: Public domain W3C validator