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

Theorem prid2g 4516
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 4515 . 2 (𝐵𝑉𝐵 ∈ {𝐵, 𝐴})
2 prcom 4487 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
31, 2syl6eleq 2916 1 (𝐵𝑉𝐵 ∈ {𝐴, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2164  {cpr 4401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-sn 4400  df-pr 4402
This theorem is referenced by:  prel12g  4616  prproe  4658  unisn2  5021  fr2nr  5324  fpr2g  6736  f1prex  6799  pw2f1olem  8339  hashprdifel  13482  gcdcllem3  15603  mgm2nsgrplem1  17766  mgm2nsgrplem2  17767  mgm2nsgrplem3  17768  sgrp2nmndlem1  17771  sgrp2rid2  17774  pmtrprfv  18230  m2detleib  20812  indistopon  21183  pptbas  21190  coseq0negpitopi  24662  uhgr2edg  26511  umgrvad2edg  26516  uspgr2v1e2w  26555  usgr2v1e2w  26556  nb3grprlem1  26685  nb3grprlem2  26686  1hegrvtxdg1  26812  prsiga  30735  ftc1anclem8  34034  fourierdlem54  41169  prsal  41327  sge0pr  41400  imarnf1pr  42183  paireqne  42279  1hegrlfgr  42578
  Copyright terms: Public domain W3C validator