Theorem prid2g 4721

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

Step	Hyp	Ref	Expression
1		prid1g 4720	. 2 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐴})
2		prcom 4692	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
3	1, 2	eleqtrdi 2873	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∈ wcel 2143  {cpr 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4584  df-pr 4586

This theorem is referenced by:  prel12g  4823  prproe  4864  unisn2  5263  fr2nr  5625  fpr2g  7196  f1prex  7269  fvf1pr  7292  pw2f1olem  9054  hashprdifel  14412  gcdcllem3  16536  chnccat  18659  mgm2nsgrplem1  18956  mgm2nsgrplem2  18957  mgm2nsgrplem3  18958  sgrp2nmndlem1  18961  sgrp2rid2  18964  pmtrprfv  19494  m2detleib  22692  indistopon  23062  pptbas  23069  coseq0negpitopi  26569  uhgr2edg  29410  umgrvad2edg  29415  uspgr2v1e2w  29453  usgr2v1e2w  29454  nb3grprlem1  29582  nb3grprlem2  29583  1hegrvtxdg1  29709  cyc3genpmlem  33332  elrspunsn  33616  esplyfval1  33871  prsiga  34429  bj-prmoore  37606  ftc1anclem8  38200  pr2el2  44128  pr2eldif2  44132  fourierdlem54  46735  prsal  46893  sge0pr  46969  imarnf1pr  47877  paireqne  48118  stgrnbgr0  48587  grlimprclnbgr  48619  1hegrlfgr  48755  lubprlem  49584  fucoppcffth  50033  uobeqterm  50168  2arwcatlem4  50220  2arwcat  50222  incat  50223