Theorem prid2g 4716

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

Syntax hints:   → wi 4   ∈ wcel 2113  {cpr 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-sn 4579  df-pr 4581

This theorem is referenced by:  prel12g  4818  prproe  4859  unisn2  5255  fr2nr  5599  fpr2g  7155  f1prex  7228  fvf1pr  7251  pw2f1olem  9007  hashprdifel  14319  gcdcllem3  16426  chnccat  18547  mgm2nsgrplem1  18841  mgm2nsgrplem2  18842  mgm2nsgrplem3  18843  sgrp2nmndlem1  18846  sgrp2rid2  18849  pmtrprfv  19380  m2detleib  22573  indistopon  22943  pptbas  22950  coseq0negpitopi  26466  uhgr2edg  29230  umgrvad2edg  29235  uspgr2v1e2w  29273  usgr2v1e2w  29274  nb3grprlem1  29402  nb3grprlem2  29403  1hegrvtxdg1  29530  cyc3genpmlem  33182  elrspunsn  33459  prsiga  34237  bj-prmoore  37259  ftc1anclem8  37840  pr2el2  43734  pr2eldif2  43738  fourierdlem54  46346  prsal  46504  sge0pr  46580  imarnf1pr  47470  paireqne  47699  stgrnbgr0  48152  grlimprclnbgr  48184  1hegrlfgr  48320  lubprlem  49149  fucoppcffth  49598  uobeqterm  49733  2arwcatlem4  49785  2arwcat  49787  incat  49788