Theorem prid2g 4766

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

Syntax hints:   → wi 4   ∈ wcel 2098  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-un 3950  df-sn 4630  df-pr 4632

This theorem is referenced by:  prel12g  4865  prproe  4906  unisn2  5312  fr2nr  5655  fpr2g  7221  f1prex  7291  pw2f1olem  9099  hashprdifel  14389  gcdcllem3  16475  mgm2nsgrplem1  18874  mgm2nsgrplem2  18875  mgm2nsgrplem3  18876  sgrp2nmndlem1  18879  sgrp2rid2  18882  pmtrprfv  19412  m2detleib  22563  indistopon  22934  pptbas  22941  coseq0negpitopi  26468  uhgr2edg  29077  umgrvad2edg  29082  uspgr2v1e2w  29120  usgr2v1e2w  29121  nb3grprlem1  29249  nb3grprlem2  29250  1hegrvtxdg1  29377  cyc3genpmlem  32929  elrspunsn  33207  prsiga  33820  bj-prmoore  36664  ftc1anclem8  37243  pr2el2  43046  pr2eldif2  43050  fourierdlem54  45611  prsal  45769  sge0pr  45845  imarnf1pr  46725  paireqne  46914  1hegrlfgr  47306  lubprlem  48093