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

Theorem prid2g 4240
 Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
Assertion
Ref Expression
prid2g (𝐵𝑉𝐵 ∈ {𝐴, 𝐵})

Proof of Theorem prid2g
StepHypRef Expression
1 prid1g 4239 . 2 (𝐵𝑉𝐵 ∈ {𝐵, 𝐴})
2 prcom 4211 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
31, 2syl6eleq 2698 1 (𝐵𝑉𝐵 ∈ {𝐴, 𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1977  {cpr 4127 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128 This theorem is referenced by:  unisn2  4722  fr2nr  5016  fpr2g  6380  f1prex  6439  pw2f1olem  7949  hashprdifel  13047  gcdcllem3  15061  mgm2nsgrplem1  17228  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  sgrp2nmndlem1  17233  sgrp2rid2  17236  pmtrprfv  17696  m2detleib  20256  indistopon  20615  pptbas  20622  coseq0negpitopi  24059  usgra2edg  25911  nb3graprlem1  25980  nb3graprlem2  25981  2trllemF  26079  vdgr1b  26431  prsiga  29521  ftc1anclem8  32662  fourierdlem54  39053  prsal  39214  sge0pr  39287  imarnf1pr  40326  uhgr2edg  40435  umgrvad2edg  40440  uspgr2v1e2w  40477  usgr2v1e2w  40478  nb3grprlem1  40608  nb3grprlem2  40609  1hegrlfgr  40722  1hegrvtxdg1  40723
 Copyright terms: Public domain W3C validator