Theorem prid2g 4706

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

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

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 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  prel12g  4808  prproe  4849  unisn2  5248  fr2nr  5602  fpr2g  7160  f1prex  7233  fvf1pr  7256  pw2f1olem  9013  hashprdifel  14354  gcdcllem3  16464  chnccat  18586  mgm2nsgrplem1  18883  mgm2nsgrplem2  18884  mgm2nsgrplem3  18885  sgrp2nmndlem1  18888  sgrp2rid2  18891  pmtrprfv  19422  m2detleib  22609  indistopon  22979  pptbas  22986  coseq0negpitopi  26483  uhgr2edg  29294  umgrvad2edg  29299  uspgr2v1e2w  29337  usgr2v1e2w  29338  nb3grprlem1  29466  nb3grprlem2  29467  1hegrvtxdg1  29594  cyc3genpmlem  33230  elrspunsn  33507  esplyfval1  33735  prsiga  34294  bj-prmoore  37446  ftc1anclem8  38038  pr2el2  43999  pr2eldif2  44003  fourierdlem54  46609  prsal  46767  sge0pr  46843  imarnf1pr  47745  paireqne  47986  stgrnbgr0  48455  grlimprclnbgr  48487  1hegrlfgr  48623  lubprlem  49452  fucoppcffth  49901  uobeqterm  50036  2arwcatlem4  50088  2arwcat  50090  incat  50091