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

Theorem prid2g 4727
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 4726 . 2 (𝐵𝑉𝐵 ∈ {𝐵, 𝐴})
2 prcom 4698 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
31, 2eleqtrdi 2848 1 (𝐵𝑉𝐵 ∈ {𝐴, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  {cpr 4593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-sn 4592  df-pr 4594
This theorem is referenced by:  prel12g  4826  prproe  4868  unisn2  5274  fr2nr  5616  fpr2g  7166  f1prex  7235  pw2f1olem  9027  hashprdifel  14305  gcdcllem3  16388  mgm2nsgrplem1  18735  mgm2nsgrplem2  18736  mgm2nsgrplem3  18737  sgrp2nmndlem1  18740  sgrp2rid2  18743  pmtrprfv  19242  m2detleib  21996  indistopon  22367  pptbas  22374  coseq0negpitopi  25876  uhgr2edg  28198  umgrvad2edg  28203  uspgr2v1e2w  28241  usgr2v1e2w  28242  nb3grprlem1  28370  nb3grprlem2  28371  1hegrvtxdg1  28497  cyc3genpmlem  32042  prsiga  32770  bj-prmoore  35615  ftc1anclem8  36187  pr2el2  41897  pr2eldif2  41901  fourierdlem54  44475  prsal  44633  sge0pr  44709  imarnf1pr  45588  paireqne  45777  1hegrlfgr  46108  lubprlem  47069
  Copyright terms: Public domain W3C validator