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 2838	1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∈ wcel 2109  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-sn 4586  df-pr 4588

This theorem is referenced by:  prel12g  4824  prproe  4865  unisn2  5262  fr2nr  5608  fpr2g  7167  f1prex  7241  fvf1pr  7264  pw2f1olem  9022  hashprdifel  14339  gcdcllem3  16447  mgm2nsgrplem1  18827  mgm2nsgrplem2  18828  mgm2nsgrplem3  18829  sgrp2nmndlem1  18832  sgrp2rid2  18835  pmtrprfv  19367  m2detleib  22551  indistopon  22921  pptbas  22928  coseq0negpitopi  26445  uhgr2edg  29188  umgrvad2edg  29193  uspgr2v1e2w  29231  usgr2v1e2w  29232  nb3grprlem1  29360  nb3grprlem2  29361  1hegrvtxdg1  29488  cyc3genpmlem  33123  elrspunsn  33393  prsiga  34114  bj-prmoore  37096  ftc1anclem8  37687  pr2el2  43533  pr2eldif2  43537  fourierdlem54  46151  prsal  46309  sge0pr  46385  imarnf1pr  47276  paireqne  47505  stgrnbgr0  47956  1hegrlfgr  48113  lubprlem  48943  fucoppcffth  49393  uobeqterm  49528  2arwcatlem4  49580  2arwcat  49582  incat  49583