Theorem prid2g 4729

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  prel12g  4831  prproe  4872  unisn2  5277  fr2nr  5640  fpr2g  7216  f1prex  7291  fvf1pr  7314  pw2f1olem  9076  hashprdifel  14454  gcdcllem3  16583  chnccat  18706  mgm2nsgrplem1  19019  mgm2nsgrplem2  19020  mgm2nsgrplem3  19021  sgrp2nmndlem1  19024  sgrp2rid2  19027  pmtrprfv  19569  m2detleib  22840  indistopon  23210  pptbas  23217  coseq0negpitopi  26721  uhgr2edg  29618  umgrvad2edg  29623  uspgr2v1e2w  29661  usgr2v1e2w  29662  nb3grprlem1  29790  nb3grprlem2  29791  1hegrvtxdg1  29917  cyc3genpmlem  33537  elrspunsn  33803  esplyfval1  34029  prsiga  34587  bj-prmoore  37816  ftc1anclem8  38410  pr2el2  44337  pr2eldif2  44341  fourierdlem54  46934  prsal  47092  sge0pr  47168  imarnf1pr  48079  paireqne  48320  stgrnbgr0  48789  grlimprclnbgr  48821  1hegrlfgr  48957  lubprlem  49799  fucoppcffth  50248  uobeqterm  50383  2arwcatlem4  50435  2arwcat  50437  incat  50438