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

Theorem prid2g 4271
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 4270 . 2 (𝐵𝑉𝐵 ∈ {𝐵, 𝐴})
2 prcom 4242 . 2 {𝐵, 𝐴} = {𝐴, 𝐵}
31, 2syl6eleq 2714 1 (𝐵𝑉𝐵 ∈ {𝐴, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1992  {cpr 4155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-un 3565  df-sn 4154  df-pr 4156
This theorem is referenced by:  unisn2  4759  fr2nr  5057  fpr2g  6430  f1prex  6494  pw2f1olem  8009  hashprdifel  13123  gcdcllem3  15142  mgm2nsgrplem1  17321  mgm2nsgrplem2  17322  mgm2nsgrplem3  17323  sgrp2nmndlem1  17326  sgrp2rid2  17329  pmtrprfv  17789  m2detleib  20351  indistopon  20710  pptbas  20717  coseq0negpitopi  24154  uhgr2edg  25987  umgrvad2edg  25992  uspgr2v1e2w  26030  usgr2v1e2w  26031  nb3grprlem1  26163  nb3grprlem2  26164  1hegrvtxdg1  26283  prsiga  29967  ftc1anclem8  33110  fourierdlem54  39671  prsal  39832  sge0pr  39905  imarnf1pr  40586  1hegrlfgr  40989
  Copyright terms: Public domain W3C validator