Theorem prid2g 4732

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

Syntax hints:   → wi 4   ∈ wcel 2149  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  prel12g  4833  prproe  4874  unisn2  5277  fr2nr  5639  fpr2g  7210  f1prex  7283  fvf1pr  7306  pw2f1olem  9069  hashprdifel  14434  gcdcllem3  16559  chnccat  18682  mgm2nsgrplem1  18980  mgm2nsgrplem2  18981  mgm2nsgrplem3  18982  sgrp2nmndlem1  18985  sgrp2rid2  18988  pmtrprfv  19523  m2detleib  22757  indistopon  23127  pptbas  23134  coseq0negpitopi  26634  uhgr2edg  29499  umgrvad2edg  29504  uspgr2v1e2w  29542  usgr2v1e2w  29543  nb3grprlem1  29671  nb3grprlem2  29672  1hegrvtxdg1  29798  cyc3genpmlem  33412  elrspunsn  33681  esplyfval1  33908  prsiga  34466  bj-prmoore  37679  ftc1anclem8  38273  pr2el2  44203  pr2eldif2  44207  fourierdlem54  46800  prsal  46958  sge0pr  47034  imarnf1pr  47942  paireqne  48183  stgrnbgr0  48652  grlimprclnbgr  48684  1hegrlfgr  48820  lubprlem  49659  fucoppcffth  50108  uobeqterm  50243  2arwcatlem4  50295  2arwcat  50297  incat  50298