Theorem prid2g 4711

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

Syntax hints:   → wi 4   ∈ wcel 2111  {cpr 4575

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576

This theorem is referenced by:  prel12g  4813  prproe  4854  unisn2  5248  fr2nr  5591  fpr2g  7145  f1prex  7218  fvf1pr  7241  pw2f1olem  8994  hashprdifel  14305  gcdcllem3  16412  chnccat  18532  mgm2nsgrplem1  18826  mgm2nsgrplem2  18827  mgm2nsgrplem3  18828  sgrp2nmndlem1  18831  sgrp2rid2  18834  pmtrprfv  19365  m2detleib  22546  indistopon  22916  pptbas  22923  coseq0negpitopi  26439  uhgr2edg  29186  umgrvad2edg  29191  uspgr2v1e2w  29229  usgr2v1e2w  29230  nb3grprlem1  29358  nb3grprlem2  29359  1hegrvtxdg1  29486  cyc3genpmlem  33120  elrspunsn  33394  prsiga  34144  bj-prmoore  37159  ftc1anclem8  37739  pr2el2  43643  pr2eldif2  43647  fourierdlem54  46257  prsal  46415  sge0pr  46491  imarnf1pr  47381  paireqne  47610  stgrnbgr0  48063  grlimprclnbgr  48095  1hegrlfgr  48231  lubprlem  49061  fucoppcffth  49511  uobeqterm  49646  2arwcatlem4  49698  2arwcat  49700  incat  49701