Theorem prid2g 4718

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

Syntax hints:   → wi 4   ∈ wcel 2113  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  prel12g  4820  prproe  4861  unisn2  5257  fr2nr  5601  fpr2g  7157  f1prex  7230  fvf1pr  7253  pw2f1olem  9011  hashprdifel  14323  gcdcllem3  16430  chnccat  18551  mgm2nsgrplem1  18845  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem1  18850  sgrp2rid2  18853  pmtrprfv  19384  m2detleib  22577  indistopon  22947  pptbas  22954  coseq0negpitopi  26470  uhgr2edg  29283  umgrvad2edg  29288  uspgr2v1e2w  29326  usgr2v1e2w  29327  nb3grprlem1  29455  nb3grprlem2  29456  1hegrvtxdg1  29583  cyc3genpmlem  33235  elrspunsn  33512  prsiga  34290  bj-prmoore  37322  ftc1anclem8  37903  pr2el2  43813  pr2eldif2  43817  fourierdlem54  46425  prsal  46583  sge0pr  46659  imarnf1pr  47549  paireqne  47778  stgrnbgr0  48231  grlimprclnbgr  48263  1hegrlfgr  48399  lubprlem  49228  fucoppcffth  49677  uobeqterm  49812  2arwcatlem4  49864  2arwcat  49866  incat  49867