Theorem prid2g 4727

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3921  df-sn 4592  df-pr 4594

This theorem is referenced by:  prel12g  4830  prproe  4871  unisn2  5269  fr2nr  5617  fpr2g  7187  f1prex  7261  fvf1pr  7284  pw2f1olem  9049  hashprdifel  14369  gcdcllem3  16477  mgm2nsgrplem1  18851  mgm2nsgrplem2  18852  mgm2nsgrplem3  18853  sgrp2nmndlem1  18856  sgrp2rid2  18859  pmtrprfv  19389  m2detleib  22524  indistopon  22894  pptbas  22901  coseq0negpitopi  26418  uhgr2edg  29141  umgrvad2edg  29146  uspgr2v1e2w  29184  usgr2v1e2w  29185  nb3grprlem1  29313  nb3grprlem2  29314  1hegrvtxdg1  29441  cyc3genpmlem  33114  elrspunsn  33406  prsiga  34127  bj-prmoore  37098  ftc1anclem8  37689  pr2el2  43533  pr2eldif2  43537  fourierdlem54  46151  prsal  46309  sge0pr  46385  imarnf1pr  47273  paireqne  47502  stgrnbgr0  47953  1hegrlfgr  48110  lubprlem  48940  fucoppcffth  49390  uobeqterm  49525  2arwcatlem4  49577  2arwcat  49579  incat  49580