Theorem prid2g 4705

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  prel12g  4807  prproe  4848  unisn2  5247  fr2nr  5608  fpr2g  7166  f1prex  7239  fvf1pr  7262  pw2f1olem  9019  hashprdifel  14360  gcdcllem3  16470  chnccat  18592  mgm2nsgrplem1  18889  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  sgrp2nmndlem1  18894  sgrp2rid2  18897  pmtrprfv  19428  m2detleib  22596  indistopon  22966  pptbas  22973  coseq0negpitopi  26467  uhgr2edg  29277  umgrvad2edg  29282  uspgr2v1e2w  29320  usgr2v1e2w  29321  nb3grprlem1  29449  nb3grprlem2  29450  1hegrvtxdg1  29576  cyc3genpmlem  33212  elrspunsn  33489  esplyfval1  33717  prsiga  34275  bj-prmoore  37427  ftc1anclem8  38021  pr2el2  43978  pr2eldif2  43982  fourierdlem54  46588  prsal  46746  sge0pr  46822  imarnf1pr  47730  paireqne  47971  stgrnbgr0  48440  grlimprclnbgr  48472  1hegrlfgr  48608  lubprlem  49437  fucoppcffth  49886  uobeqterm  50021  2arwcatlem4  50073  2arwcat  50075  incat  50076