Theorem prid2g 4697

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cpr 4563

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  prel12g  4794  prproe  4837  unisn2  5236  fr2nr  5567  fpr2g  7087  f1prex  7156  pw2f1olem  8863  hashprdifel  14113  gcdcllem3  16208  mgm2nsgrplem1  18557  mgm2nsgrplem2  18558  mgm2nsgrplem3  18559  sgrp2nmndlem1  18562  sgrp2rid2  18565  pmtrprfv  19061  m2detleib  21780  indistopon  22151  pptbas  22158  coseq0negpitopi  25660  uhgr2edg  27575  umgrvad2edg  27580  uspgr2v1e2w  27618  usgr2v1e2w  27619  nb3grprlem1  27747  nb3grprlem2  27748  1hegrvtxdg1  27874  cyc3genpmlem  31418  prsiga  32099  bj-prmoore  35286  ftc1anclem8  35857  pr2el2  41158  pr2eldif2  41162  fourierdlem54  43701  prsal  43859  sge0pr  43932  imarnf1pr  44774  paireqne  44963  1hegrlfgr  45294  lubprlem  46256