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

Theorem prid2g 4328
 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 4327 . 2 (𝐵𝑉𝐵 ∈ {𝐵, 𝐴})
2 prcom 4299 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
31, 2syl6eleq 2740 1 (𝐵𝑉𝐵 ∈ {𝐴, 𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2030  {cpr 4212 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213 This theorem is referenced by:  prproe  4466  unisn2  4827  fr2nr  5121  fpr2g  6516  f1prex  6579  pw2f1olem  8105  hashprdifel  13224  gcdcllem3  15270  mgm2nsgrplem1  17452  mgm2nsgrplem2  17453  mgm2nsgrplem3  17454  sgrp2nmndlem1  17457  sgrp2rid2  17460  pmtrprfv  17919  m2detleib  20485  indistopon  20853  pptbas  20860  coseq0negpitopi  24300  uhgr2edg  26145  umgrvad2edg  26150  uspgr2v1e2w  26188  usgr2v1e2w  26189  nb3grprlem1  26326  nb3grprlem2  26327  1hegrvtxdg1  26459  prsiga  30322  ftc1anclem8  33622  fourierdlem54  40695  prsal  40856  sge0pr  40929  imarnf1pr  41624  1hegrlfgr  42038
 Copyright terms: Public domain W3C validator