Theorem prid2g 4720

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 4719	. 2 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐴})
2		prcom 4691	. 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵}
3	1, 2	eleqtrdi 2847	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∈ wcel 2114  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  prel12g  4822  prproe  4863  unisn2  5259  fr2nr  5609  fpr2g  7167  f1prex  7240  fvf1pr  7263  pw2f1olem  9021  hashprdifel  14333  gcdcllem3  16440  chnccat  18561  mgm2nsgrplem1  18858  mgm2nsgrplem2  18859  mgm2nsgrplem3  18860  sgrp2nmndlem1  18863  sgrp2rid2  18866  pmtrprfv  19397  m2detleib  22590  indistopon  22960  pptbas  22967  coseq0negpitopi  26483  uhgr2edg  29297  umgrvad2edg  29302  uspgr2v1e2w  29340  usgr2v1e2w  29341  nb3grprlem1  29469  nb3grprlem2  29470  1hegrvtxdg1  29597  cyc3genpmlem  33249  elrspunsn  33526  esplyfval1  33754  prsiga  34313  bj-prmoore  37372  ftc1anclem8  37955  pr2el2  43911  pr2eldif2  43915  fourierdlem54  46522  prsal  46680  sge0pr  46756  imarnf1pr  47646  paireqne  47875  stgrnbgr0  48328  grlimprclnbgr  48360  1hegrlfgr  48496  lubprlem  49325  fucoppcffth  49774  uobeqterm  49909  2arwcatlem4  49961  2arwcat  49963  incat  49964